diff options
Diffstat (limited to 'src/main/Makefile.am')
| -rw-r--r-- | src/main/Makefile.am | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/src/main/Makefile.am b/src/main/Makefile.am index 594751358..730afa32d 100644 --- a/src/main/Makefile.am +++ b/src/main/Makefile.am @@ -65,6 +65,9 @@ smt2_tokens.h: @srcdir@/../parser/smt2/Smt2.g tptp_tokens.h: @srcdir@/../parser/tptp/Tptp.g $(AM_V_GEN)grep "'[a-zA-Z][a-zA-Z0-9][a-zA-Z0-9]*'" $^ | sed 's/.*'\''\([a-zA-Z0-9]*\)'\''.*/"\1",/' | sort -u >$@ +EXTRA_DIST = \ + options_handlers.h + clean-local: rm -f $(BUILT_SOURCES) |