summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorAndres Noetzli <noetzli@stanford.edu>2017-07-15 12:27:17 -0700
committerAndres Noetzli <noetzli@stanford.edu>2017-07-15 12:27:17 -0700
commit0703c4e7665421d701c5823f33b010ef04ffa3a6 (patch)
tree08165a7f041ad041404c880695544b1c12819987
parent9c56063e64e0613dee5b41e9b4750fe6e6550b81 (diff)
-rw-r--r--src/parser/tptp/Makefile.am1
1 files changed, 1 insertions, 0 deletions
diff --git a/src/parser/tptp/Makefile.am b/src/parser/tptp/Makefile.am
index eab01103f..43bbc595d 100644
--- a/src/parser/tptp/Makefile.am
+++ b/src/parser/tptp/Makefile.am
@@ -5,6 +5,7 @@ AM_CXXFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN) $(WNO_PARENTH
# Compile generated C files using C++ compiler
AM_CFLAGS = $(AM_CXXFLAGS)
+CFLAGS=$(CXXFLAGS)
CC=$(CXX)
ANTLR_OPTS =
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback