aboutsummaryrefslogtreecommitdiffstats
path: root/src/configure.sh
diff options
context:
space:
mode:
Diffstat (limited to 'src/configure.sh')
-rwxr-xr-xsrc/configure.sh9
1 files changed, 5 insertions, 4 deletions
diff --git a/src/configure.sh b/src/configure.sh
index 85571cd..3def21c 100755
--- a/src/configure.sh
+++ b/src/configure.sh
@@ -2,9 +2,10 @@
pre=$(echo $0 | sed "s,\(\([^/]*/\)*\)[^/]*,\1,")
-rm -f ${pre}Make
+rm -f ${pre}_CoqProject
rm -f ${pre}Makefile
rm -f ${pre}Makefile.conf
+rm -f ${pre}Makefile.local
rm -f ${pre}smtcoq_plugin.ml4
rm -f ${pre}versions/native/Structures.v
rm -f ${pre}g_smtcoq.ml4
@@ -23,7 +24,8 @@ if [ $@ -a $@ = -native ]; then
cp ${pre}versions/native/smtcoq_plugin_native.ml4 ${pre}smtcoq_plugin.ml4
cp ${pre}versions/native/Structures_native.v ${pre}versions/native/Structures.v
else
- cp ${pre}versions/standard/Make ${pre}Make
+ cp ${pre}versions/standard/_CoqProject ${pre}_CoqProject
+ cp ${pre}versions/standard/Makefile.local ${pre}Makefile.local
cp ${pre}versions/standard/g_smtcoq_standard.ml4 ${pre}g_smtcoq.ml4
cp ${pre}versions/standard/smtcoq_plugin_standard.mlpack ${pre}smtcoq_plugin.mlpack
cp ${pre}versions/standard/Int63/Int63_standard.v ${pre}versions/standard/Int63/Int63.v
@@ -33,6 +35,5 @@ else
cp ${pre}versions/standard/Int63/Int63Properties_standard.v ${pre}versions/standard/Int63/Int63Properties.v
cp ${pre}versions/standard/Array/PArray_standard.v ${pre}versions/standard/Array/PArray.v
cp ${pre}versions/standard/Structures_standard.v ${pre}versions/standard/Structures.v
- coq_makefile -f Make -o Makefile
- sed -i Makefile -e "s/ocamldep/ocamldep -native/" -e "s/ \$(HIDE)\$(MAKE) --no-print-directory -f \"\$(SELF)\" post-all//"
+ coq_makefile -f _CoqProject -o Makefile
fi