diff options
Diffstat (limited to 'src/Makefile.am')
| -rw-r--r-- | src/Makefile.am | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/src/Makefile.am b/src/Makefile.am index 944600c81..a46f56598 100644 --- a/src/Makefile.am +++ b/src/Makefile.am @@ -70,6 +70,7 @@ install-data-local: $(publicheaders) uninstall-local: @for f in $(publicheaders); do \ - rm -f "$(DESTDIR)/$(includedir)/cvc4/$$f" + f=`echo "$$f" | sed 's,.*/,,'`; \ + rm -f "$(DESTDIR)$(includedir)/cvc4/$$f"; \ done - rmdir "$(DESTDIR)/$(includedir)/cvc4" + @rmdir "$(DESTDIR)$(includedir)/cvc4" |