diff options
author | Morgan Deters <mdeters@cs.nyu.edu> | 2014-03-19 16:32:05 -0400 |
---|---|---|
committer | Morgan Deters <mdeters@cs.nyu.edu> | 2014-03-19 16:37:32 -0400 |
commit | ea22ebcbd69b24906d2214b7d294261578ce67a7 (patch) | |
tree | e64d46a849d4e40f544bbb9199fe08e3fce7ef58 /src/util | |
parent | 5ca5dd42d95ce08a4ea456212fffcd2672e31fc1 (diff) |
Set dumping options from (set-option..) and API more directly.
Diffstat (limited to 'src/util')
-rw-r--r-- | src/util/dump.h | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/util/dump.h b/src/util/dump.h index 0bde68d76..a85062af1 100644 --- a/src/util/dump.h +++ b/src/util/dump.h @@ -14,7 +14,7 @@ ** Dump utility classes and functions. **/ -#include "cvc4_public.h" +#include "cvc4_private.h" #ifndef __CVC4__DUMP_H #define __CVC4__DUMP_H |