diff options
author | Morgan Deters <mdeters@gmail.com> | 2012-11-09 17:39:05 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2012-11-09 17:39:05 +0000 |
commit | d11716a24a2b70b7c3681e52de51bd622c4f6447 (patch) | |
tree | 0206e07556f8c21d0c48c8f8a960b810fe4e66f6 /Makefile.am | |
parent | cad60d99f8fe38dd5098d14958d2dd844bbe6584 (diff) |
another DISTCLEANFILES entry, for proper "make distclean" behavior (fixes "distclean" target error last night)
Diffstat (limited to 'Makefile.am')
-rw-r--r-- | Makefile.am | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/Makefile.am b/Makefile.am index efa4a068a..5ddde3cad 100644 --- a/Makefile.am +++ b/Makefile.am @@ -147,6 +147,7 @@ distclean-local: DISTCLEANFILES = \ doc/cvc4.1 \ doc/cvc4.1_template \ + doc/pcvc4.1 \ doc/cvc4.5 \ doc/libcvc4.3 \ doc/libcvc4.3_template \ |