From 03fce0a33fe639652adb414398c9970b05f0e811 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 10 Jan 2017 13:24:32 +0100
Subject: [PATCH] awk.Makefile: uninstall .v and .glob files
---
awk.Makefile | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/awk.Makefile b/awk.Makefile
index 268f6f686..09ded0aa6 100644
--- a/awk.Makefile
+++ b/awk.Makefile
@@ -13,7 +13,7 @@
# Also see <https://coq.inria.fr/bugs/show_bug.cgi?id=4907>.
/^uninstall:/ {
print "uninstall:";
- print "\tif [ -d \"$(DSTROOT)\"$(COQLIBINSTALL)/"PROJECT"/ ]; then find \"$(DSTROOT)\"$(COQLIBINSTALL)/"PROJECT"/ \\( -name \"*.vo\" -o \\( -type d -empty \\) \\) -print -delete; fi";
+ 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
}
--
GitLab