diff options
| author | Maxime Dénès | 2017-09-22 11:20:13 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-09-22 11:20:13 +0200 |
| commit | 6d3b6c3c1f798ace3b57048401069ec52532d6ed (patch) | |
| tree | 8d7a44889c35d6aee02eaafce2c0fb232e3bcbbe | |
| parent | 809fab2fde0c8dbd8ea940c563be9ab5f988d9d0 (diff) | |
| parent | ddf7b82220a504a8af3ac6d2dfc9664300a1db82 (diff) | |
Merge PR #1064: coq_makefile: dont show errors from failed (ignored) rmdir
| -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 56e12a1e06..afe8e62ee3 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 |