From b062ccfd70d17f52d21bd59e0d0a55029f9df440 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Mon, 26 Dec 2016 00:44:57 +0100 Subject: [PATCH] add `make watch` --- Makefile | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) diff --git a/Makefile b/Makefile index 9908566..69c58f4 100644 --- a/Makefile +++ b/Makefile @@ -80,4 +80,10 @@ update_next_tag: sed -i "s/NEXT_VERSION/$(VERSION)/g" *.ml *.mli sed -i "s/NEXT_RELEASE/$(VERSION)/g" *.ml *.mli -.PHONY: benchs tests examples update_next_tag push_doc push_stable +watch: + while find src/ -print0 | xargs -0 inotifywait -e delete_self -e modify ; do \ + echo "============ at `date` ==========" ; \ + make all; \ + done + +.PHONY: benchs tests examples update_next_tag push_doc push_stable watch