diff options
| author | Morgan Deters <mdeters@gmail.com> | 2012-05-09 21:52:38 +0000 |
|---|---|---|
| committer | Morgan Deters <mdeters@gmail.com> | 2012-05-09 21:52:38 +0000 |
| commit | 6a4af721d1dc55f1dc6454014c08f87465398a54 (patch) | |
| tree | 178f006869c0c4af6b6c71f46b55c28de643c7bd /src/util/Makefile.am | |
| parent | 1ce0650dcf8ce30424b546deb540974cc510c215 (diff) | |
--disable-tracing at configure time now disables Trace() and Debug() gestures both.
Diffstat (limited to 'src/util/Makefile.am')
| -rw-r--r-- | src/util/Makefile.am | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/src/util/Makefile.am b/src/util/Makefile.am index 87fa2c890..dddcbb38c 100644 --- a/src/util/Makefile.am +++ b/src/util/Makefile.am @@ -88,6 +88,7 @@ BUILT_SOURCES = \ integer.h \ tls.h if CVC4_DEBUG +if CVC4_TRACING # listing Debug_tags too ensures that make doesn't auto-remove it # after building (if it does, we don't get the "cached" effect with # the .tmp files below, and we have to re-compile and re-link each @@ -96,6 +97,7 @@ BUILT_SOURCES += \ Debug_tags.h \ Debug_tags endif +endif if CVC4_TRACING # listing Trace_tags too ensures that make doesn't auto-remove it # after building (if it does, we don't get the "cached" effect with |