awk.Makefile: uninstall .v and .glob files

03fce0a3 · Ralf Jung · b356673e · 03fce0a3
Commit 03fce0a3 authored Jan 10, 2017 by Ralf Jung
Hide whitespace changes
Inline Side-by-side

Showing with 1 addition and 1 deletion

awk.Makefile awk.Makefile +1 -1

No files found.
--- 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
 }