diff --git a/Makefile b/Makefile index 25526672..4f0e4731 100644 --- a/Makefile +++ b/Makefile @@ -128,4 +128,10 @@ devel: --enable-bigarray --enable-thread --enable-advanced make all +watch: + while find src/ -print0 | xargs -0 inotifywait -e delete_self -e modify ; do \ + echo "============ at `date` ==========" ; \ + make ; \ + done + .PHONY: examples push_doc tags qtest-gen qtest-clean devel update_next_tag