summaryrefslogtreecommitdiff
path: root/src/expr/expr_manager_template.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/expr/expr_manager_template.cpp')
-rw-r--r--src/expr/expr_manager_template.cpp6
1 files changed, 0 insertions, 6 deletions
diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp
index 0d22a3c41..bac9e3b43 100644
--- a/src/expr/expr_manager_template.cpp
+++ b/src/expr/expr_manager_template.cpp
@@ -26,12 +26,6 @@
${includes}
-// This is a hack, but an important one: if there's an error, the
-// compiler directs the user to the template file instead of the
-// generated one. We don't want the user to modify the generated one,
-// since it'll get overwritten on a later build.
-#line 34 "${template}"
-
#ifdef CVC4_STATISTICS_ON
#define INC_STAT(kind) \
{ \
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback