Closed nishaq503 closed 2 months ago
This PR also edits github actions to ignore files that were deleted and lets them succeed when there are no updated tools. See the status of the checks below for how that looks.
This PR also edits github actions to ignore files that were deleted and lets them succeed when there are no updated tools. See the status of the checks below for how that looks.