aboutsummaryrefslogtreecommitdiff
path: root/dev
diff options
context:
space:
mode:
Diffstat (limited to 'dev')
-rwxr-xr-xdev/lint-repository.sh2
1 files changed, 1 insertions, 1 deletions
diff --git a/dev/lint-repository.sh b/dev/lint-repository.sh
index 224601bbce..553696410c 100755
--- a/dev/lint-repository.sh
+++ b/dev/lint-repository.sh
@@ -33,6 +33,6 @@ echo Checking overlays
dev/tools/check-overlays.sh || CODE=1
echo Checking ocamlformat
-dune build @fmt || CODE=1
+make -f Makefile.dune fmt || CODE=1
exit $CODE