summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--src/util/gmp_util.h2
-rw-r--r--test/system/Makefile.am3
2 files changed, 3 insertions, 2 deletions
diff --git a/src/util/gmp_util.h b/src/util/gmp_util.h
index e8054fe6b..f884ddca6 100644
--- a/src/util/gmp_util.h
+++ b/src/util/gmp_util.h
@@ -17,7 +17,7 @@
** \todo document this file
**/
-#include "cvc4_private.h"
+#include "cvc4_public.h"
#ifndef __CVC4__GMP_UTIL_H
#define __CVC4__GMP_UTIL_H
diff --git a/test/system/Makefile.am b/test/system/Makefile.am
index 0f80aa454..cc0d63aee 100644
--- a/test/system/Makefile.am
+++ b/test/system/Makefile.am
@@ -17,7 +17,8 @@ TEST_DEPS_DIST = \
cvc3_main.cpp \
cvc3_george.h \
cvc3_george.cpp \
- CVC4JavaTest.java
+ CVC4JavaTest.java \
+ run_java_test
# Make-level dependencies; these don't go in the source distribution
# but should trigger a re-compile of all unit tests. Libraries are
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback