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