From ca0be4274dd7593c44db46670d078095e9f6c1c7 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 26 Sep 2017 12:41:22 +0200
Subject: [PATCH] awk.Makefile: Don't patch vio2vo; instead add quick2vo
---
awk.Makefile | 11 +++++------
1 file changed, 5 insertions(+), 6 deletions(-)
diff --git a/awk.Makefile b/awk.Makefile
index 74f7d570..91f7d737 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
--
GitLab