Skip to content
GitLab
Projects
Groups
Snippets
/
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Menu
Open sidebar
Jonas Kastberg
iris
Commits
b356673e
Commit
b356673e
authored
Jan 10, 2017
by
Ralf Jung
Browse files
awk.Makefile: uninstall: also delete empty directories
parent
fc9f3bc3
Changes
1
Hide whitespace changes
Inline
Side-by-side
awk.Makefile
View file @
b356673e
...
...
@@ -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
}
...
...
Write
Preview
Supports
Markdown
0%
Try again
or
attach a new file
.
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment