diff options
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 |