diff --git a/Makefile b/Makefile index ae9d00fb9..26d6e441e 100644 --- a/Makefile +++ b/Makefile @@ -48,4 +48,4 @@ reindent: @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: all benchs test clean build doc update_next_tag watch +.PHONY: all benchs test clean build doc update_next_tag watch examples