summaryrefslogtreecommitdiff
path: root/src/options
diff options
context:
space:
mode:
authorMathias Preiner <mathias.preiner@gmail.com>2018-03-24 23:38:34 -0700
committerAndres Noetzli <andres.noetzli@gmail.com>2018-03-24 23:38:34 -0700
commit9e9e6b8777047160ef7a1f2708a295aa503eb856 (patch)
tree032a6be349042de48aa470d8f4e7d9e953a88dd5 /src/options
parent22586fb55f88ea964c723716af9ea43cf3f93c87 (diff)
Remove doc/libcvc4.3 from options/Makefile.am. (#1696)
This commit fixes an issue with calling make clean && make. The final doc/libcvc4.3 is now generated during ./autogen.sh and should not be deleted with make clean.
Diffstat (limited to 'src/options')
-rw-r--r--src/options/Makefile.am2
1 files changed, 0 insertions, 2 deletions
diff --git a/src/options/Makefile.am b/src/options/Makefile.am
index 723b110ea..edcc9eb9c 100644
--- a/src/options/Makefile.am
+++ b/src/options/Makefile.am
@@ -120,7 +120,6 @@ CLEANFILES = \
$(OPTIONS_GEN_H) \
$(OPTIONS_GEN_CPP) \
$(DOCUMENTATION_FILES) \
- ../../doc/libcvc4.3 \
options_holder.h
@@ -132,7 +131,6 @@ EXTRA_DIST = \
$(OPTIONS_CONFIG_FILES) \
$(CPP_TEMPLATE_FILES) \
$(DOCUMENTATION_FILES) \
- ../../doc/libcvc4.3 \
mkoptions.py \
language.i \
option_exception.i \
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback