diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2017-06-01 15:41:36 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2017-06-01 15:43:02 +0200 |
| commit | 305c8dc1a8518388077c5f2d063f793a2c2e39da (patch) | |
| tree | 8a45cee731719c7410eb981d84a201b92e9bc0fe /tools | |
| parent | f3a388baf9cf2a14a658cab77554a0802b999486 (diff) | |
Fix coq_makefile uninstall target under OSX.
Diffstat (limited to 'tools')
| -rw-r--r-- | tools/CoqMakefile.in | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in index fb064c495..1308e9175 100644 --- a/tools/CoqMakefile.in +++ b/tools/CoqMakefile.in @@ -375,7 +375,7 @@ uninstall:: instf="$(DESTDIR)$(COQLIBINSTALL)/$$df/`basename $$f`"; \ rm -f "$$instf";\ echo RM "$$instf"; \ - rmdir --ignore-fail-on-non-empty "$(DESTDIR)$(COQLIBINSTALL)/$$df/"; \ + rmdir "$(DESTDIR)$(COQLIBINSTALL)/$$df/" || true; \ done .PHONY: uninstall @@ -385,8 +385,7 @@ uninstall-doc:: $(HIDE)rm -rf "$(DESTDIR)$(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/html" $(SHOW)'RM $(DESTDIR)$(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/mlihtml' $(HIDE)rm -rf "$(DESTDIR)$(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/mlihtml" - $(HIDE)rmdir --ignore-fail-on-non-empty \ - "$(DESTDIR)$(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/" + $(HIDE) rmdir "$(DESTDIR)$(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/" || true .PHONY: uninstall-doc # Cleaning #################################################################### |