diff --git a/Makefile b/Makefile index ce07e4f6..296149db 100644 --- a/Makefile +++ b/Makefile @@ -137,4 +137,9 @@ watch: make all; \ done +reindent: + @which ocp-indent || ( echo "require ocp-indent" ; exit 1 ) + @find src '(' -name '*.ml' -or -name '*.mli' ')' -type f -print0 | xargs -0 echo "reindenting: " + @find src '(' -name '*.ml' -or -name '*.mli' ')' -type f -print0 | xargs -0 ocp-indent -i + .PHONY: examples push_doc tags qtest-gen qtest-clean devel update_next_tag