diff options
| author |  Ralf Jung <post@ralfj.de> | 2017-09-20 11:51:17 +0200 |
|---|---|---|
| committer | Ralf Jung <post@ralfj.de> | 2017-09-20 13:53:00 +0200 |
| commit | ddf7b82220a504a8af3ac6d2dfc9664300a1db82 (patch) | |
| tree | 3f216435d63ac0797d770869c2b30a3384a6de25 /tools | |
| parent | 9933871efd122163f7e2dfe8377b9b2dd384b47b (diff) | |
coq_makefile: dont show errors from failed (ignored) rmdir
Diffstat (limited to 'tools')
| -rw-r--r-- | tools/CoqMakefile.in | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in index 56e12a1e0..afe8e62ee 100644 --- a/tools/CoqMakefile.in +++ b/tools/CoqMakefile.in @@ -500,7 +500,7 @@ uninstall:: instf="$(COQLIBINSTALL)/$$df/`basename $$f`" &&\ rm -f "$$instf" &&\ echo RM "$$instf" &&\ - (rmdir "$(call concat_path,,$(COQLIBINSTALL)/$$df/)" || true); \ + (rmdir "$(call concat_path,,$(COQLIBINSTALL)/$$df/)" 2>/dev/null || true); \ done .PHONY: uninstall |