diff --git a/Makefile b/Makefile index 5a2a346439b83a409f5da00519400b2e3aef9594..7d2ef1b295146f35dd116dc99de1fd2a1c35e2db 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 dc1c7eee18ec6f3d5f1530e777e707dc9c1ff393..0000000000000000000000000000000000000000 --- 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