projects / cvc5.git / commitdiff
? search:
summary | shortlog | log | commit | commitdiff | tree
raw | patch | inline | side by side (parent: 7801622)
another make distclean fix
authorMorgan Deters <mdeters@gmail.com>
Mon, 31 Oct 2011 21:25:07 +0000 (21:25 +0000)
committerMorgan Deters <mdeters@gmail.com>
Mon, 31 Oct 2011 21:25:07 +0000 (21:25 +0000)
Makefile patch | blob | history

diff --git a/Makefile b/Makefile
index 8cf0fbcc242e1afcf7011072e0867e93eed64c4e..5f1b42f0e9c50cfa52a4e99f7f342c76d9daa500 100644 (file)
--- a/Makefile
+++ b/Makefile
@@ -28,6 +28,7 @@ distclean maintainerclean:
                $(MAKE) $@; \
        fi
        test -z "$(builddir)" || rm -fr "$(builddir)"
+       rm -f config.reconfig
 
 # synonyms for "check"
 .PHONY: test