From df509b210516c6a28c4979496a874699813dccca Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 8 Nov 2018 11:48:22 +0100
Subject: [PATCH] remove no-longer-needed Makefile hackery
---
Makefile | 4 +---
awk.Makefile | 23 -----------------------
2 files changed, 1 insertion(+), 26 deletions(-)
delete mode 100644 awk.Makefile
diff --git a/Makefile b/Makefile
index 5a2a3464..7d2ef1b2 100644
--- a/Makefile
+++ b/Makefile
@@ -12,11 +12,9 @@ clean: Makefile.coq
rm -f Makefile.coq
.PHONY: clean
-# Create Coq Makefile. POSIX awk can't do in-place editing, but coq_makefile wants the real
-# filename, so we do some file gymnastics.
+# Create Coq Makefile.
Makefile.coq: _CoqProject Makefile awk.Makefile
"$(COQBIN)coq_makefile" -f _CoqProject -o Makefile.coq
- mv Makefile.coq Makefile.coq.tmp && awk -f awk.Makefile Makefile.coq.tmp > Makefile.coq && rm Makefile.coq.tmp
# Install build-dependencies
build-dep/opam: opam Makefile
diff --git a/awk.Makefile b/awk.Makefile
deleted file mode 100644
index dc1c7eee..00000000
--- a/awk.Makefile
+++ /dev/null
@@ -1,23 +0,0 @@
-# awk program that patches the Makefile generated by Coq.
-
-# Detect the name this project will be installed under.
-/\$\(COQLIBINSTALL\)\/.*\/\$\$i/ {
-# Wow, POSIX awk is really broken. I mean, isn't it supposed to be a text processing language?
-# And there is not even a way to access the matched groups of a regexp...?!? Lucky enough,
-# we can just split the string at '/' here.
- split($0, PIECES, /\//);
- PROJECT=PIECES[2];
-}
-
-# Patch the uninstall target to work properly, and to also uninstall stale files.
-# Also see <https://coq.inria.fr/bugs/show_bug.cgi?id=4907>.
-# This (and the section above) can be removed once we no longer support Coq 8.6.
-/^uninstall: / {
- print "uninstall:";
- print "\tif [ -d \"$(DSTROOT)\"$(COQLIBINSTALL)/"PROJECT"/ ]; then find \"$(DSTROOT)\"$(COQLIBINSTALL)/"PROJECT"/ \\( -name \"*.vo\" -o -name \"*.v\" -o -name \"*.glob\" -o \\( -type d -empty \\) \\) -print -delete; fi";
- getline;
- next
-}
-
-# This forwards all unchanged lines
-1
--
GitLab