Philip Chimento 7fc86bca6a Migrate linter workflow to GitHub Actions ... This runs faster and allows for future improvements. I'm following a general principle of keeping code that isn't portable between CI providers inside the config file for the CI provider. So in this case we remove the Circle-CI-specific stuff from the file in tools/scripts/, and into .github/workflows/. We use an external action (tj-actions/changed-files) to gather the list of files to lint.		2024-11-11 16:48:38 -08:00
..
ci_build.sh	CI: show result of "git status --porcelain"	2020-09-25 13:16:06 -04:00
ci_lint.sh	Migrate linter workflow to GitHub Actions	2024-11-11 16:48:38 -08:00
ci_test.sh	CI: Do not report test failures as errors	2021-05-28 18:06:58 -04:00