aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
-rw-r--r--src/Make.native (renamed from src/Make)3
-rw-r--r--src/Makefile.native (renamed from src/Makefile)2
-rwxr-xr-xsrc/configure.sh9
3 files changed, 10 insertions, 4 deletions
diff --git a/src/Make b/src/Make.native
index d1c9342..34e6dc2 100644
--- a/src/Make
+++ b/src/Make.native
@@ -27,7 +27,6 @@
-I verit
-I zchaff
-# -custom "cd ../unit-tests; make" "" "logs"
-custom "cd ../unit-tests; make" "" "test"
-custom "$(CAMLLEX) $<" "%.mll" "%.ml"
@@ -87,5 +86,3 @@ SMTCoq.v
SMT_terms.v
State.v
Trace.v
-
-# tests/Tests.v
diff --git a/src/Makefile b/src/Makefile.native
index 8919e7f..2ec982f 100644
--- a/src/Makefile
+++ b/src/Makefile.native
@@ -14,7 +14,7 @@
#
# This Makefile was generated by the command line :
-# coq_makefile -f Make -o Makefile
+# coq_makefile -f Make.native -o Makefile
#
.DEFAULT_GOAL := all
diff --git a/src/configure.sh b/src/configure.sh
new file mode 100755
index 0000000..04da739
--- /dev/null
+++ b/src/configure.sh
@@ -0,0 +1,9 @@
+#!/bin/sh
+
+set -e
+
+if [ $@ -a $@ = -standard ]; then
+ cp Makefile.standard Makefile
+else
+ cp Makefile.native Makefile
+fi