Def writeJsonFile

Modification history

2023-11-19 18:46
scripts/runMathlibLinter.lean
chore: use Std's runLinter (#8461)
Deleted writeJsonFileView on Github →
2022-06-13 18:50
scripts/runLinter.lean
perf: compile runLinter.lean (#285) …
Added writeJsonFileView on Github →