diff options
Diffstat (limited to 'dev/tools/pre-commit')
| -rwxr-xr-x | dev/tools/pre-commit | 13 |
1 files changed, 11 insertions, 2 deletions
diff --git a/dev/tools/pre-commit b/dev/tools/pre-commit index 633913aac6..448e224f2e 100755 --- a/dev/tools/pre-commit +++ b/dev/tools/pre-commit @@ -16,6 +16,15 @@ then 1>&2 echo "Warning: ocamlformat is not in path. Cannot check formatting." fi +# Verify that the version of ocamlformat matches the one in .ocamlformat +# The following command will print an error message if that's not the case +# (and will print nothing if the versions match) +if ! echo "let () = ()" | "$ocamlformat" --impl - > /dev/null +then + 1>&2 echo "Warning: Cannot check formatting." + ocamlformat=true +fi + 1>&2 echo "Auto fixing whitespace and formatting issues..." # We fix whitespace in the index and in the working tree @@ -43,7 +52,7 @@ if [ -s "$index" ]; then git apply --cached --whitespace=fix "$index" git apply --whitespace=fix "$index" 2>/dev/null # no need to repeat yourself git diff --cached --name-only -z | xargs -0 dev/tools/check-eof-newline.sh --fix - git diff --cached --name-only -z | grep -E '.*\.mli?$' -z | xargs -0 "$ocamlformat" -i || true + { git diff --cached --name-only -z | grep -E '.*\.mli?$' -z | xargs -0 "$ocamlformat" -i || true; } 2> /dev/null git add -u 1>&2 echo #newline fi @@ -59,7 +68,7 @@ if [ -s "$tree" ]; then 1>&2 echo "Fixing unstaged changes..." git apply --whitespace=fix "$tree" git diff --name-only -z | xargs -0 dev/tools/check-eof-newline.sh --fix - git diff --name-only -z | grep -E '.*\.mli?$' -z | xargs -0 "$ocamlformat" -i || true + { git diff --name-only -z | grep -E '.*\.mli?$' -z | xargs -0 "$ocamlformat" -i || true; } 2> /dev/null 1>&2 echo #newline fi |