From 389bbaa3a88fde9e1d8712fbcc3185af0f8856a0 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 3 Apr 2018 11:58:01 +0200
Subject: [PATCH] update CI and build system
---
awk.Makefile | 12 ------------
ci | 2 +-
2 files changed, 1 insertion(+), 13 deletions(-)
diff --git a/awk.Makefile b/awk.Makefile
index 91f7d737..dc1c7eee 100644
--- a/awk.Makefile
+++ b/awk.Makefile
@@ -19,17 +19,5 @@
next
}
-# 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 "quick2vo:";
- print "\t@make -j $(J) quick"
- 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 $(TIMER) $(COQC) $(COQDEBUG) $(COQFLAGS) -schedule-vio2vo $(J) $$VIOFILES; fi"
- print ".PHONY: quick2vo"
-}
-
# This forwards all unchanged lines
1
diff --git a/ci b/ci
index b58c3b6d..d2edcd47 160000
--- a/ci
+++ b/ci
@@ -1 +1 @@
-Subproject commit b58c3b6db3087e19b01e54ec640b465e7262935e
+Subproject commit d2edcd474159cc883d09c0a08dbd463c2d2780df
--
GitLab