Commit 2023-11-19 18:46 7b0cbe23

View on Github →

chore: use Std's runLinter (#8461)

Estimated changes

Modified .github/workflows/bors.yml

Modified .github/workflows/build.yml

Modified .github/workflows/build.yml.in

Modified .github/workflows/build_fork.yml

Modified GNUmakefile

Modified lakefile.lean

Deleted scripts/runMathlibLinter.lean

deleted def readJsonFile

deleted def writeJsonFile