diff --git a/awk.Makefile b/awk.Makefile index 7ac6aa41b29e7f091a4e2b31a70920a722ec7331..268f6f6866e08f67965c186949f31964e25da50c 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\" -print -delete; fi"; + print "\tif [ -d \"$(DSTROOT)\"$(COQLIBINSTALL)/"PROJECT"/ ]; then find \"$(DSTROOT)\"$(COQLIBINSTALL)/"PROJECT"/ \\( -name \"*.vo\" -o \\( -type d -empty \\) \\) -print -delete; fi"; getline; next }