From 8ba7983f467a6e235ba88e10be90381c9429cad2 Mon Sep 17 00:00:00 2001
From: Pierre Letouzey
Date: Sat, 30 Nov 2013 11:04:10 +0100
Subject: 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
---
 dev/ocamldebug-coq.run      | 34 ++++++++++++++++++++++++++++++++++
 dev/ocamldebug-coq.template | 29 -----------------------------
 2 files changed, 34 insertions(+), 29 deletions(-)
 create mode 100644 dev/ocamldebug-coq.run
 delete mode 100644 dev/ocamldebug-coq.template

(limited to 'dev')

diff --git a/dev/ocamldebug-coq.run b/dev/ocamldebug-coq.run
new file mode 100644
index 0000000000..aab03f34d9
--- /dev/null
+++ b/dev/ocamldebug-coq.run
@@ -0,0 +1,34 @@
+#!/bin/sh
+
+# Wrapper around ocamldebug for Coq
+
+# 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 \
+	-I $COQTOP \
+	-I $COQTOP/config -I $COQTOP/printing -I $COQTOP/grammar \
+	-I $COQTOP/lib -I $COQTOP/intf -I $COQTOP/kernel \
+	-I $COQTOP/library -I $COQTOP/pretyping -I $COQTOP/parsing \
+        -I $COQTOP/interp -I $COQTOP/proofs -I $COQTOP/tactics \
+	-I $COQTOP/toplevel -I $COQTOP/dev -I $COQTOP/config \
+        -I $COQTOP/plugins/cc         -I $COQTOP/plugins/dp \
+        -I $COQTOP/plugins/extraction -I $COQTOP/plugins/field \
+        -I $COQTOP/plugins/firstorder -I $COQTOP/plugins/fourier \
+        -I $COQTOP/plugins/funind     -I $COQTOP/plugins/groebner \
+        -I $COQTOP/plugins/interface  -I $COQTOP/plugins/micromega \
+        -I $COQTOP/plugins/omega      -I $COQTOP/plugins/quote \
+        -I $COQTOP/plugins/ring       -I $COQTOP/plugins/romega \
+	-I $COQTOP/plugins/rtauto     -I $COQTOP/plugins/setoid_ring \
+        -I $COQTOP/plugins/subtac     -I $COQTOP/plugins/syntax \
+        -I $COQTOP/plugins/xml \
+        -I $COQTOP/ide \
+	"$@"
diff --git a/dev/ocamldebug-coq.template b/dev/ocamldebug-coq.template
deleted file mode 100644
index ffe4c6b402..0000000000
--- a/dev/ocamldebug-coq.template
+++ /dev/null
@@ -1,29 +0,0 @@
-#!/bin/sh
-
-# wrap around ocamldebug for Coq
-
-export COQTOP=COQTOPDIRECTORY
-CAMLBIN=CAMLBINDIRECTORY
-CAMLP4LIB=CAMLP4LIBDIRECTORY
-OCAMLDEBUG=$CAMLBIN/ocamldebug
-
-exec $OCAMLDEBUG \
-	-I $CAMLP4LIB \
-	-I $COQTOP \
-	-I $COQTOP/config -I $COQTOP/printing -I $COQTOP/grammar \
-	-I $COQTOP/lib -I $COQTOP/intf -I $COQTOP/kernel \
-	-I $COQTOP/library -I $COQTOP/pretyping -I $COQTOP/parsing \
-        -I $COQTOP/interp -I $COQTOP/proofs -I $COQTOP/tactics \
-	-I $COQTOP/toplevel -I $COQTOP/dev -I $COQTOP/config \
-        -I $COQTOP/plugins/cc         -I $COQTOP/plugins/dp \
-        -I $COQTOP/plugins/extraction -I $COQTOP/plugins/field \
-        -I $COQTOP/plugins/firstorder -I $COQTOP/plugins/fourier \
-        -I $COQTOP/plugins/funind     -I $COQTOP/plugins/groebner \
-        -I $COQTOP/plugins/interface  -I $COQTOP/plugins/micromega \
-        -I $COQTOP/plugins/omega      -I $COQTOP/plugins/quote \
-        -I $COQTOP/plugins/ring       -I $COQTOP/plugins/romega \
-	-I $COQTOP/plugins/rtauto     -I $COQTOP/plugins/setoid_ring \
-        -I $COQTOP/plugins/subtac     -I $COQTOP/plugins/syntax \
-        -I $COQTOP/plugins/xml \
-        -I $COQTOP/ide \
-	$*
-- 
cgit v1.2.3