From 264e89b1981b020786881b0f27fda04cdb2beec2 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Sat, 14 Dec 2019 16:32:24 -0600 Subject: [PATCH] chore: makefile --- Makefile | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Makefile b/Makefile index ae9d00fb..26d6e441 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