diff options
| author | Pierre-Marie Pédrot | 2020-09-23 11:12:44 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-09-28 09:28:41 +0200 |
| commit | 3a88c57442c0c9a5e23a25d04e3695d6e61587c3 (patch) | |
| tree | 85a81686b74acd0a174b8a001f615f20f75909bd /dev | |
| parent | 7b28475547cc2391034f3e61437777d4513e9094 (diff) | |
Remove the linter ocamlformat pass.
Diffstat (limited to 'dev')
| -rwxr-xr-x | dev/lint-repository.sh | 3 |
1 files changed, 0 insertions, 3 deletions
diff --git a/dev/lint-repository.sh b/dev/lint-repository.sh index 553696410c..2e8a7455de 100755 --- a/dev/lint-repository.sh +++ b/dev/lint-repository.sh @@ -32,7 +32,4 @@ find . "(" -path ./.git -prune ")" -o -type f -print0 | echo Checking overlays dev/tools/check-overlays.sh || CODE=1 -echo Checking ocamlformat -make -f Makefile.dune fmt || CODE=1 - exit $CODE |