aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorChantal Keller <Chantal.Keller@inria.fr>2015-01-13 15:51:35 +0100
committerChantal Keller <Chantal.Keller@inria.fr>2015-01-13 15:51:35 +0100
commit469a88043ad000403cff5122e27770c130ef77e4 (patch)
tree24504b11d1de17f5ec6db23683314339116b4e76
parent44a7c303c34dabd68e8d28c7de6ee54cc03a774b (diff)
downloadsmtcoq-469a88043ad000403cff5122e27770c130ef77e4.tar.gz
smtcoq-469a88043ad000403cff5122e27770c130ef77e4.zip
Room for compilation with other versions of Coq
-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