aboutsummaryrefslogtreecommitdiff
path: root/dev
diff options
context:
space:
mode:
authorPierre Letouzey2013-11-30 11:04:10 +0100
committerPierre Letouzey2013-12-20 18:57:08 +0100
commit8ba7983f467a6e235ba88e10be90381c9429cad2 (patch)
tree57d30e939d0e366d59809d3d335fb767cc4d5e91 /dev
parentd1824e8e6f472385d790c52792c7bf4a5adde41d (diff)
configure.ml: our configure script is now written in ML :-)
configure is now just a minimal wrapper around the new configure.ml. This configure.ml is runned with the same ocaml used during compilation, and starts with a #load "unix.cma". For now, this new configure script is meant to be 99% compatible with the old one. Known incompatibilities : the --foo option format (with two --) isn't supported anymore, use -foo options instead. Let me know if you encounter any other changes. Internals: - We use our own "run" command (based on Unix.create_process) to avoid relying on some specific shell (/bin/sh or cmd.exe). - We should have far less issues with filename quoting under windows since we almost never rely on (cygwin) shell anymore. This remains to be fully tested, though. - dev/ocamldebug-coq is slightly different now, to ease its generation
Diffstat (limited to 'dev')
-rw-r--r--dev/ocamldebug-coq.run (renamed from dev/ocamldebug-coq.template)17
1 files changed, 11 insertions, 6 deletions
diff --git a/dev/ocamldebug-coq.template b/dev/ocamldebug-coq.run
index ffe4c6b402..aab03f34d9 100644
--- a/dev/ocamldebug-coq.template
+++ b/dev/ocamldebug-coq.run
@@ -1,11 +1,16 @@
#!/bin/sh
-# wrap around ocamldebug for Coq
+# Wrapper around ocamldebug for Coq
-export COQTOP=COQTOPDIRECTORY
-CAMLBIN=CAMLBINDIRECTORY
-CAMLP4LIB=CAMLP4LIBDIRECTORY
-OCAMLDEBUG=$CAMLBIN/ocamldebug
+# This file is to be launched via the generated script ocamldebug-coq,
+# which will set the env variables $OCAMLDEBUG, $CAMLP4LIB, $COQTOP
+# Anyway, just in case someone tries to use this script directly,
+# here are some reasonable default values
+
+[ -z "$OCAMLDEBUG" ] && OCAMLDEBUG=ocamldebug
+[ -z "$CAMLP4LIB" ] && CAMLP4LIB=+camlp5
+[ -z "$COQTOP" -a -d "$PWD/kernel" ] && COQTOP=$PWD
+[ -z "$COQTOP" -a -d "$PWD/../kernel" ] && COQTOP=`dirname $PWD`
exec $OCAMLDEBUG \
-I $CAMLP4LIB \
@@ -26,4 +31,4 @@ exec $OCAMLDEBUG \
-I $COQTOP/plugins/subtac -I $COQTOP/plugins/syntax \
-I $COQTOP/plugins/xml \
-I $COQTOP/ide \
- $*
+ "$@"