diff --git a/awk.Makefile b/awk.Makefile index 74f7d5705b7b0aa240eb66fd0f3645beb064b1ab..91f7d7374d1fd76f61ef2f9404ba4e1b1ac3dfb7 100644 --- a/awk.Makefile +++ b/awk.Makefile @@ -19,17 +19,16 @@ next } -# Patch vio2vo to (a) run "make quick" with the same number of jobs, ensuring +# Add new target quick2vo to (a) run "make quick" with the same number of jobs, ensuring # that the .vio files are up-to-date, and (b) only schedule vio2vo for those # files where the .vo is *older* than the .vio. /^vio2vo:/ { - print "vio2vo:"; + print "quick2vo:"; print "\t@make -j $(J) quick" - print "\t@VIOFILES=$$(for file in $(VOFILES:%.vo=%.vio); do vofile=\"$$(echo \"$$file\" | sed \"s/\\.vio/.vo/\")\"; if [ \"$$vofile\" -ot \"$$file\" -o ! -e \"$$vofile\" ]; then echo -n \"$$file \"; fi; done); \\" + print "\t@VIOFILES=$$(for vofile in $(VOFILES); do viofile=\"$$(echo \"$$vofile\" | sed \"s/\\.vo/.vio/\")\"; if [ \"$$vofile\" -ot \"$$viofile\" -o ! -e \"$$vofile\" ]; then echo -n \"$$viofile \"; fi; done); \\" print "\t echo \"VIO2VO: $$VIOFILES\"; \\" - print "\t if [ -n \"$$VIOFILES\" ]; then $(COQC) $(COQDEBUG) $(COQFLAGS) -schedule-vio2vo $(J) $$VIOFILES; fi" - getline; - next + print "\t if [ -n \"$$VIOFILES\" ]; then $(TIMER) $(COQC) $(COQDEBUG) $(COQFLAGS) -schedule-vio2vo $(J) $$VIOFILES; fi" + print ".PHONY: quick2vo" } # This forwards all unchanged lines