chore: makefile

c-cube · Dec 14, 2019 · 264e89b · 264e89b
1 parent 138047e
commit 264e89b
Showing 1 changed file with 1 addition and 1 deletion.
diff --git 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