Imported Upstream version 8.5~beta1+dfsg

1 files changed, 24 insertions, 1281 deletions

diff --git a/configure b/configure
index cb43a73d..09585e59 100755
--- a/configure
+++ b/configure
@@ -1,1294 +1,37 @@
 #!/bin/sh
 
-##################################
-#
-#  Configuration script for Coq
-# 
-##################################
+## This micro-configure shell script is here only to
+## launch the real configuration via ocaml
 
-VERSION=8.4pl4
-VOMAGIC=08400
-STATEMAGIC=58400
-DATE=`LC_ALL=C LANG=C date +"%B %Y"`
+cmd=ocaml
+script=./configure.ml
 
-# Create the bin/ directory if non-existent
-test -d bin || mkdir bin
-
-# a local which command for sh
-which () {
-IFS=":" # set words separator in PATH to be ':' (it allows spaces in dirnames)
-for i in $PATH; do
-  if test -z "$i"; then i=.; fi 
-  if [ -f "$i/$1" ] ; then
-	IFS=" "
-        echo "$i/$1"
-	break
-  fi
-done
-}
-
-usage () {
-    printf "Available options for configure are:\n"
-    echo "-help"
-    printf "\tDisplays this help page\n"
-    echo "-prefix <dir>"
-    printf "\tSet installation directory to <dir>\n"
-    echo "-local"
-    printf "\tSet installation directory to the current source tree\n"
-    echo "-coqrunbyteflags <flags>"
-    printf "\tSet link flags for VM-dependent bytecode (coqtop)\n"
-    echo "-coqtoolsbyteflags <flags>"
-    printf "\tSet link flags for VM-independant bytecode (coqdep, coqdoc, ...)\n"
-    echo "-custom"
-    printf "\tGenerate all bytecode executables with -custom (not recommended)\n"
-    echo "-src <dir>"
-    printf "\tSpecifies the source directory\n"
-    echo "-bindir <dir>"
-    echo "-libdir <dir>"
-    echo "-configdir <dir>"
-    echo "-datadir <dir>"
-    echo "-mandir <dir>"
-    echo "-docdir <dir>"
-    printf "\tSpecifies where to install bin/lib/config/data/man/doc files resp.\n"
-    echo "-emacslib <dir>"
-    printf "\tSpecifies where emacs files are to be installed\n"
-    echo "-coqdocdir <dir>"
-    printf "\tSpecifies where Coqdoc style files are to be installed\n"
-    echo "-camldir <dir>"
-    printf "\tSpecifies the path to the OCaml library\n"
-    echo "-lablgtkdir <dir>"
-    printf "\tSpecifies the path to the Lablgtk library\n"
-    echo "-usecamlp5"
-    printf "\tSpecifies to use camlp5 instead of camlp4\n"
-    echo "-usecamlp4"
-    printf "\tSpecifies to use camlp4 instead of camlp5\n"
-    echo "-camlp5dir <dir>"
-    printf "\tSpecifies where to look for the Camlp5 library and tells to use it\n"
-    echo "-arch <arch>"
-    printf "\tSpecifies the architecture\n"
-    echo "-opt"
-    printf "\tSpecifies whether or not to use OCaml *.opt optimized compilers\n"
-    echo "-natdynlink (yes|no)"
-    printf "\tSpecifies whether or not to use dynamic loading of native code\n"
-    echo "-coqide (opt|byte|no)"
-    printf "\tSpecifies whether or not to compile Coqide\n"
-    echo "-nomacintegration"
-    printf "\tSpecifies to not try to build coqide mac integration\n"
-    echo "-browser <command>"
-    printf "\tUse <command> to open URL %%s\n"
-    echo "-with-doc (yes|no)"
-    printf "\tSpecifies whether or not to compile the documentation\n"
-    echo "-with-geoproof (yes|no)"
-    printf "\tSpecifies whether or not to use Geoproof binding\n"
-    echo "-byte-only"
-    printf "\tCompiles only bytecode version of Coq\n"
-    echo "-debug"
-    printf "\tAdd debugging information in the Coq executables\n"
-    echo "-profile"
-    printf "\tAdd profiling information in the Coq executables\n"
-    echo "-annotate"
-    printf "\tCompiles Coq with -dtypes option\n"
-    echo "-makecmd <command>"
-    printf "\tName of GNU Make command.\n"
-}
-
-
-# Default OCaml binaries
-bytecamlc=ocamlc
-nativecamlc=ocamlopt
-ocamlmklibexec=ocamlmklib
-ocamlexec=ocaml
-ocamldepexec=ocamldep
-ocamldocexec=ocamldoc
-ocamllexexec=ocamllex
-ocamlyaccexec=ocamlyacc
-ocamlmktopexec=ocamlmktop
-camlp4oexec=camlp4o
-
-
-coq_debug_flag=
-coq_debug_flag_opt=
-coq_profile_flag=
-coq_annotate_flag=
-best_compiler=opt
-cflags="-Wall -Wno-unused"
-natdynlink=yes
-
-local=false
-coqrunbyteflags_spec=no
-coqtoolsbyteflags_spec=no
-custom_spec=no
-src_spec=no
-prefix_spec=no
-bindir_spec=no
-libdir_spec=no
-configdir_spec=no
-datadir_spec=no
-mandir_spec=no
-docdir_spec=no
-emacslib_spec=no
-emacs_spec=no
-camldir_spec=no
-lablgtkdir_spec=no
-coqdocdir_spec=no
-arch_spec=no
-coqide_spec=no
-nomacintegration_spec=no
-browser_spec=no
-wwwcoq_spec=no
-with_geoproof=false
-with_doc=all
-with_doc_spec=no
-force_caml_version=no
-force_caml_version_spec=no
-usecamlp5=yes
-
-COQSRC=`pwd`
-
-# Parse command-line arguments
-
-while : ; do
-  case "$1" in
-    "") break;;
-    -help|--help) usage
-	          exit;;
-    -prefix|--prefix) prefix_spec=yes
-                      prefix="$2"
-		      shift;;
-    -local|--local) local=true;;
-    -coqrunbyteflags|--coqrunbyteflags) coqrunbyteflags_spec=yes
-                                        coqrunbyteflags="$2"
-                                        shift;;
-    -coqtoolsbyteflags|--coqtoolsbyteflags) coqtoolsbyteflags_spec=yes
-                                            coqtoolsbyteflags="$2"
-                                            shift;;
-    -custom|--custom) custom_spec=yes;;
-    -src|--src) src_spec=yes
-                COQSRC="$2"
-	        shift;;
-    -bindir|--bindir) bindir_spec=yes
-                      bindir="$2"
-		      shift;;
-    -libdir|--libdir) libdir_spec=yes
-                      libdir="$2"
-		      shift;;
-    -configdir|--configdir) configdir_spec=yes
-                      configdir="$2"
-		      shift;;
-    -datadir|--datadir) datadir_spec=yes
-                      datadir="$2"
-		      shift;;
-    -mandir|--mandir) mandir_spec=yes
-                      mandir="$2"
-		      shift;;
-    -docdir|--docdir) docdir_spec=yes
-                      docdir="$2"
-		      shift;;
-    -emacslib|--emacslib) emacslib_spec=yes
-                          emacslib="$2"
-			  shift;;
-    -emacs |--emacs) emacs_spec=yes
-		     emacs="$2"
-                     printf "Warning: obsolete -emacs option\n"
-		     shift;;
-    -coqdocdir|--coqdocdir) coqdocdir_spec=yes
-	              coqdocdir="$2"
-		      shift;;
-    -camldir|--camldir) camldir_spec=yes
-	                camldir="$2"
-			shift;;
-    -lablgtkdir|--lablgtkdir) lablgtkdir_spec=yes
-	                lablgtkdir="$2"
-			shift;;
-    -usecamlp5|--usecamlp5)
-	                usecamlp5=yes;;
-    -usecamlp4|--usecamlp4)
-	                usecamlp5=no;;
-    -camlp5dir|--camlp5dir)
-                        usecamlp5=yes
-	                camlp5dir="$2"
-			shift;;
-    -arch|--arch) arch_spec=yes
-                  arch=$2
-		  shift;;
-    -opt|--opt) bytecamlc=ocamlc.opt
-                camlp4oexec=camlp4o  # can't add .opt since dyn load'll be required
-                nativecamlc=ocamlopt.opt;;
-    -natdynlink|--natdynlink) case "$2" in
-	                  yes) natdynlink=yes;;
-                          *) natdynlink=no
-                        esac
-                        shift;;
-    -coqide|--coqide) coqide_spec=yes
-		      case "$2" in
-			  byte|opt) COQIDE=$2;;
-			  *) COQIDE=no
-		      esac
-		      shift;;
-    -nomacintegration) nomacintegration_spec=yes
-		      shift;;
-    -browser|--browser) browser_spec=yes
-		      BROWSER=$2
-		      shift;;
-    -coqwebsite|--coqwebsite) wwwcoq_spec=yes
-                      WWWCOQ=$2
-                      shift;;
-    -with-doc|--with-doc) with_doc_spec=yes
-		      case "$2" in
-			  yes|all) with_doc=all;;
-			  *) with_doc=no
-		      esac
-		      shift;;
-    -with-geoproof|--with-geoproof) 
-	  case "$2" in
-	      yes) with_geoproof=true;;
-	      no) with_geoproof=false;;
-	  esac
-	  shift;;
-    -makecmd|--makecmd) makecmd="$2"
-		      shift;;
-    -byte-only|-byteonly|--byteonly|--byte-only) best_compiler=byte;;
-    -debug|--debug) coq_debug_flag=-g;;
-    -profile|--profile) coq_profile_flag=-p;;
-    -annotate|--annotate) coq_annotate_flag=-dtypes;;
-    -force-caml-version|--force-caml-version|-force-ocaml-version|--force-ocaml-version) 
-          force_caml_version_spec=yes
-	  force_caml_version=yes;;
-    *) echo "Unknown option \"$1\"." 1>&2; usage; exit 2;;
-  esac
-  shift
-done
-
-if [ $prefix_spec = yes -a $local = true ] ; then
-  echo "Options -prefix and -local are incompatible."
-  echo "Configure script failed!"
-  exit 1
-fi
-
-# compile date
-DATEPGM=`which date`
-case $DATEPGM in
-    "") echo "I can't find the program \"date\" in your path."
-        echo "Please give me the current date"
-	read COMPILEDATE;;
-    *)  COMPILEDATE=`LC_ALL=C LANG=C date +"%b %d %Y %H:%M:%S"`;;
-esac
-
-# Architecture
-
-case $arch_spec in
-    no) 
-    # First we test if we are running a Cygwin or Mingw/Msys system
-    if [ `uname -s | cut -c -6` = "CYGWIN" ] ; then
-	ARCH="win32"
-	CYGWIN=yes
-    elif [ `uname -s | cut -c -7` = "MINGW32" ]; then
-	ARCH="win32"
-    else
-	# If not, we determine the architecture
-	if test -x /bin/uname ; then
- 	    ARCH=`/bin/uname -s`
- 	elif test -x /usr/bin/uname ; then
- 	    ARCH=`/usr/bin/uname -s`
- 	elif test -x /bin/arch ; then
- 	    ARCH=`/bin/arch`
- 	elif test -x /usr/bin/arch ; then
- 	    ARCH=`/usr/bin/arch`
- 	elif test -x /usr/ucb/arch ; then
- 	    ARCH=`/usr/ucb/arch`
-	else
-	    echo "I can not automatically find the name of your architecture."
-	    printf "%s"\
-		"Give me a name, please [win32 for Win95, Win98 or WinNT]: "
-	    read ARCH
-	fi
-    fi;;
-    yes) ARCH=$arch
-esac
-
-# executable extension
-
-case $ARCH in
-    win32) 
-      EXE=".exe"
-      DLLEXT=".dll";;
-    *) EXE=""
-       DLLEXT=".so"
-esac
-
-# Is the source tree checked out from a recognised
-# version control system ?
-if test -e .svn/entries ; then 
-    checkedout=svn
-elif [ -d '{arch}' ]; then
-    checkedout=gnuarch
-elif [ -z "${GIT_DIR}" ] && [ -d .git ] || [ -d "${GIT_DIR}" ]; then
-    checkedout=git
-else
-    checkedout=0
-fi
-
-# make command
-
-MAKE=`which ${makecmd:-make}`
-if [ "$MAKE" != "" ]; then
-  # Beware of the final \r in Win32
-  MAKEVERSION=`"$MAKE" -v | head -1 | tr -d "\r" | cut -d" " -f3`
-  MAKEVERSIONMAJOR=`echo $MAKEVERSION | cut -d. -f1`
-  MAKEVERSIONMINOR=`echo $MAKEVERSION | cut -d. -f2`
-  if [ "$MAKEVERSIONMAJOR" -gt 3 -o "$MAKEVERSIONMAJOR" -eq 3 -a "$MAKEVERSIONMINOR" -ge 81 ]; then
-      echo "You have GNU Make $MAKEVERSION. Good!"
-  else
-      OK="no"
-      #Extra support for local installation of make 3.81
-      #will be useless when make >= 3.81 will be standard
-      if [ -x ./make ]; then
-	  MAKEVERSION=`./make -v | head -1`
-	  if [ "$MAKEVERSION" = "GNU Make 3.81" ]; then OK="yes"; fi
-      fi
-      if [ $OK = "no" ]; then
-	  echo "GNU Make >= 3.81 is needed."
-	  echo "Make 3.81 can be downloaded from ftp://ftp.gnu.org/gnu/make/make-3.81.tar.gz"
-	  echo "then locally installed on a Unix-style system by issuing:"
-	  echo "  tar xzvf make-3.81.tar.gz"
-	  echo "  cd make-3.81"
-          echo "  ./configure"
-          echo "  make"
-          echo "  mv make .."
-	  echo "  cd .."
-	  echo "Restart then the configure script and later use ./make instead of make."
-	  exit 1
-      else
-	  echo "You have locally installed GNU Make 3.81. Good!"
-      fi
-  fi
-else
-  echo "Cannot find GNU Make >= 3.81."
-fi
-
-# Browser command
-
-if [ "$browser_spec" = "no" ]; then
-    case $ARCH in
-        win32) BROWSER='start %s' ;;
-	Darwin) BROWSER='open %s' ;;
-        *) BROWSER='firefox -remote "OpenURL(%s,new-tab)" || firefox %s &' ;;
-    esac
-fi
-
-if [ "$wwwcoq_spec" = "no" ]; then
-    WWWCOQ="http://coq.inria.fr/"
-fi
-
-#########################################
-# Objective Caml programs
-
-case $camldir_spec in
-    no) CAMLC=`which $bytecamlc`
-	case "$CAMLC" in
-	    "") echo "$bytecamlc is not present in your path!"
-		echo "Give me manually the path to the $bytecamlc executable [/usr/local/bin by default]: "
-		read CAMLC
-		
-		case "$CAMLC" in
-		    "") CAMLC=/usr/local/bin/$bytecamlc;;
-		    */ocamlc|*/ocamlc.opt) true;;
-		    */) CAMLC="${CAMLC}"$bytecamlc;;
-		    *) CAMLC="${CAMLC}"/$bytecamlc;;
-		esac
-	esac
-	CAMLBIN=`dirname "$CAMLC"`;;
-    yes) CAMLC=$camldir/$bytecamlc
-        
-         CAMLBIN=`dirname "$CAMLC"`
-	 bytecamlc="$CAMLC"
-	 nativecamlc=$CAMLBIN/$nativecamlc
-	 ocamlexec=$CAMLBIN/ocaml
-	 ocamldepexec=$CAMLBIN/ocamldep
-	 ocamldocexec=$CAMLBIN/ocamldoc
-	 ocamllexexec=$CAMLBIN/ocamllex
-	 ocamlyaccexec=$CAMLBIN/ocamlyacc
-	 ocamlmktopexec=$CAMLBIN/ocamlmktop
-	 ocamlmklibexec=$CAMLBIN/ocamlmklib
-	 camlp4oexec=$CAMLBIN/camlp4o
-esac
-
-if test ! -f "$CAMLC" ; then
-    echo "I can not find the executable '$CAMLC'. Have you installed it?"
+if [ ! -f $script ]; then
+    echo "Error: file $script not found in the current directory."
+    echo "Please run the configure script from the root of the coq sources."
     echo "Configuration script failed!"
     exit 1
 fi
 
-# Under Windows, we need to convert from cygwin/mingw paths (/c/Program Files/Ocaml)
-# to more windows-looking paths (c:/Program Files/Ocaml). Note that / are kept
-
-mk_win_path () {
-    case $ARCH,$CYGWIN in
-	win32,yes) cygpath -m "$1" ;;
-	win32*) "$ocamlexec" "tools/mingwpath.ml" "$1" ;;
-	*) echo "$1" ;;
-    esac
-}
-
-case $ARCH,$src_spec in
-    win32,yes) echo "Error: the -src option is currently not supported on Windows"
-	       exit 1;;
-    win32) CAMLBIN=`mk_win_path "$CAMLBIN"`;;
-esac
-
-# Beware of the final \r in Win32
-CAMLVERSION=`"$CAMLC" -version | tr -d "\r"`
-CAMLLIB=`"$CAMLC" -where | tr -d "\r"`
-
-case $CAMLVERSION in
-    1.*|2.*|3.0*|3.10*|3.11.[01])
-	echo "Your version of Objective-Caml is $CAMLVERSION."
-	if [ "$force_caml_version" = "yes" ]; then
-	    echo "*Warning* You are compiling Coq with an outdated version of Objective-Caml."
-	else
-	    echo "          You need Objective-Caml 3.11.2 or later."
-	    echo "          Configuration script failed!"
-	    exit 1
-	fi;;
-    3.11.2|3.12*|4.*)
-	CAMLP4COMPAT="-loc loc" 
-	echo "You have Objective-Caml $CAMLVERSION. Good!";;
-    *)
-	echo "I found the Objective-Caml compiler but cannot find its version number!"
-	echo "Is it installed properly?"
-	echo "Configuration script failed!"
-	exit 1;;
-esac
-
-CAMLTAG=OCAML`echo $CAMLVERSION | sed -e "s/\([1-9]\)\.\([0-9]*\).*/\1\2/g"`
-
-# For coqmktop & bytecode compiler
-
-if [ "$coq_debug_flag" = "-g" ]; then
-    case $CAMLTAG in
-        OCAML31*|OCAML4*)
-            # Compilation debug flag
-            coq_debug_flag_opt="-g"
-            ;;
-    esac
-fi
-
-# Native dynlink
-if [ "$natdynlink" = "yes" -a -f "$CAMLLIB"/dynlink.cmxa ]; then
-    HASNATDYNLINK=true
-else
-    HASNATDYNLINK=false
-fi
-
-case $HASNATDYNLINK,$ARCH,`uname -r`,$CAMLVERSION in
-    true,Darwin,9.*,3.11.*)  # ocaml 3.11.0 dynlink on MacOS 10.5 is buggy
-        NATDYNLINKFLAG=os5fixme;;
-    #Possibly a problem on 10.6.0/10.6.1/10.6.2
-    #May just be a 32 vs 64 problem for all 10.6.*
-    true,Darwin,10.0.*,3.11.*) # Possibly a problem on 10.6.0
-        NATDYNLINKFLAG=os5fixme;;
-    true,Darwin,10.1.*,3.11.*) # Possibly a problem on 10.6.1
-        NATDYNLINKFLAG=os5fixme;;
-    true,Darwin,10.2.*,3.11.*) # Possibly a problem on 10.6.2
-        NATDYNLINKFLAG=os5fixme;;
-    true,Darwin,10.*,3.11.*)
-        if [ `getconf LONG_BIT` = "32" ]; then
-	    # Still a problem for x86_32
-            NATDYNLINKFLAG=os5fixme
-        else
-	    # Not a problem for x86_64
-            NATDYNLINKFLAG=$HASNATDYNLINK
-        fi;;
-    *)
-        NATDYNLINKFLAG=$HASNATDYNLINK;;
-esac
-
-# Camlp4 / Camlp5 configuration
-
-# Assume that camlp(4|5) binaries are at the same place as ocaml ones
-# (this should become configurable some day)
-CAMLP4BIN=${CAMLBIN}
-
-case $usecamlp5 in
-  yes)
-    CAMLP4=camlp5
-    CAMLP4MOD=gramlib
-    if [ "$camlp5dir" != "" ]; then
-	if [ -f "$camlp5dir/${CAMLP4MOD}.cma" ]; then
-	    CAMLP4LIB=$camlp5dir
-	    FULLCAMLP4LIB=$camlp5dir
-	else
-	    echo "Cannot find camlp5 libraries in $camlp5dir (camlp5.cma not found)."
-	    echo "Configuration script failed!"
-	    exit 1
-	fi
-    else
-	# Beware of the final \r in Win32
-	camlp5dir="$(camlp5 -where | tr -d '\r')"
-	if [ "$camlp5dir" != "" ]; then
-	    CAMLP4LIB=$camlp5dir
-	    FULLCAMLP4LIB=$camlp5dir
-	elif [ -f "${CAMLLIB}/camlp5/${CAMLP4MOD}.cma" ]; then
-            CAMLP4LIB=+camlp5
-	    FULLCAMLP4LIB=${CAMLLIB}/camlp5
-	elif [ -f "${CAMLLIB}/site-lib/${CAMLP4MOD}.cma" ]; then
-        CAMLP4LIB=+site-lib/camlp5
-	FULLCAMLP4LIB=${CAMLLIB}/site-lib/camlp5
-	else
-	    echo "No Camlp5 installation found. Looking for Camlp4 instead..."
-	    usecamlp5=no
-	fi
-   fi
-esac
-
-# If we're (still...) going to use Camlp5, let's check its version
-
-case $usecamlp5 in
-  yes)
-    camlp4oexec=`echo "$camlp4oexec" | tr 4 5`
-    case `"$camlp4oexec" -v 2>&1` in
-	*"version 4.0"*|*5.00*)
-	    echo "Camlp5 version < 5.01 not supported."
-	    echo "Configuration script failed!"
-	    exit 1;;
-    esac
-esac
-
-# We might now try to use Camlp4, either by explicit choice or
-# by lack of proper Camlp5 installation
-
-case $usecamlp5 in
-  no)
-    CAMLP4=camlp4
-    CAMLP4MOD=camlp4lib
-    CAMLP4LIB=+camlp4
-    FULLCAMLP4LIB=${CAMLLIB}/camlp4
-
-    if [ ! -f "${FULLCAMLP4LIB}/${CAMLP4MOD}.cma" ]; then
-	echo "No Camlp4 installation found."
-	echo "Configuration script failed!"
-	exit 1
-    fi
-
-    camlp4oexec=${camlp4oexec}rf
-    if [ "`"$camlp4oexec" 2>&1`" != "" ]; then
-	echo "Error: $camlp4oexec not found or not executable."
-	echo "Configuration script failed!"
-	exit 1
-    fi
-esac
-
-# do we have a native compiler: test of ocamlopt and its version
-
-if [ "$best_compiler" = "opt" ] ; then
-  if test -e "$nativecamlc" || test -e "`which $nativecamlc`"; then
-      CAMLOPTVERSION=`"$nativecamlc" -v | sed -n -e 's|.*version* *\(.*\)$|\1|p' `
-      if [ ! -f "${FULLCAMLP4LIB}/${CAMLP4MOD}.cmxa" ]; then
-	  best_compiler=byte
-	  echo "Cannot find native-code $CAMLP4,"
-	  echo "only the bytecode version of Coq will be available."
-      else
-          if [ "$CAMLOPTVERSION" != "$CAMLVERSION" ] ; then
-	      echo "Native and bytecode compilers do not have the same version!"
-          fi
-          echo "You have native-code compilation. Good!"
-      fi
-  else
-      best_compiler=byte
-      echo "You have only bytecode compilation."
-  fi
-fi
-
-# OS dependent libraries
-
-OSDEPLIBS="-cclib -lunix"
-case $ARCH in
-  sun4*) OS=`uname -r`
-	case $OS in
-	   5*) OS="Sun Solaris $OS"
-	       OSDEPLIBS="$OSDEPLIBS -cclib -lnsl -cclib -lsocket";;
-	   *) OS="Sun OS $OS"
-        esac;;
-esac
-
-# lablgtk2 and CoqIDE
-
-IDEARCHFLAGS=
-IDEARCHFILE=
-IDEARCHDEF=X11
-
-# -byte-only should imply -coqide byte, unless the user decides otherwise
-
-if [ "$best_compiler" = "byte" -a "$coqide_spec" = "no" ]; then 
-    coqide_spec=yes
-    COQIDE=byte
-fi
-
-# Which coqide is asked ? which one is possible ?
-
-if [ "$coqide_spec" = "yes" -a "$COQIDE" = "no" ]; then 
-    echo "CoqIde disabled as requested."
-else
-    case $lablgtkdir_spec in
-	no)
-            # Beware of the final \r in Win32
-            lablgtkdirtmp="$(ocamlfind query lablgtk2 2> /dev/null | tr -d '\r')"
-            if [ "$lablgtkdirtmp" != "" ]; then
-                if [ -f "$lablgtkdirtmp/glib.cmi" -a -f "$lablgtkdirtmp/glib.mli" ]; then
-                    lablgtkdirfoundmsg="LabelGtk2 found by ocamlfind"
-                    lablgtkdir=$lablgtkdirtmp
-                    LABLGTKLIB=$lablgtkdir # Pour le message utilisateur
-                else
-	            echo "Headers missings in Lablgtk2 found by ocamlfind (glib.cmi/glib.mli not found)."
-                fi
-            fi
-            if [ "$lablgtkdir" = "" -a -f "${CAMLLIB}/lablgtk2/glib.cmi" -a -f "${CAMLLIB}/lablgtk2/glib.mli" ]; then
-	        lablgtkdirfoundmsg="LablGtk2 found in ocaml lib directory"
-		lablgtkdir=${CAMLLIB}/lablgtk2
-                LABLGTKLIB=+lablgtk2 # Pour le message utilisateur
-	    fi;;
-	yes)
-	    if [ ! -d "$lablgtkdir" ]; then
-                echo "$lablgtkdir is not a valid directory."
-		echo "Configuration script failed!"
-		exit 1
-	    elif [ -f "$lablgtkdir/glib.cmi" -a -f "$lablgtkdir/glib.mli" ]; then
-                lablgtkdirfoundmsg="LablGtk2 directory found"
-                LABLGTKLIB=$lablgtkdir # Pour le message utilisateur
-            else
-		echo "Headers missing in LablGtk2 library (glib.cmi/glib.mli not found)."
-		echo "Configuration script failed!"
-		exit 1
-	    fi;;
-    esac
-    if [ "$lablgtkdir" = "" ]; then
-	echo "LablGtk2 not found: CoqIde will not be available."
-	COQIDE=no
-    elif [ -z "`grep -w convert_with_fallback "$lablgtkdir/glib.mli"`" ]; then
-	echo "$lablgtkdirfoundmsg but too old: CoqIde will not be available."
-	COQIDE=no;
-    elif [ "$coqide_spec" = "yes" -a "$COQIDE" = "byte" ]; then 
-	echo "$lablgtkdirfoundmsg, bytecode CoqIde will be used as requested."
-	COQIDE=byte
-    elif [ ! -f "${CAMLLIB}/threads/threads.cmxa" ]; then 
-	echo "$lablgtkdirfoundmsg, no native threads: bytecode CoqIde will be available."
-	COQIDE=byte
-    else
-        echo "$lablgtkdirfoundmsg, native threads: native CoqIde will be available."
-	COQIDE=opt
-        if [ "$nomacintegration_spec" = "no" ] && lablgtkosxdir=$(ocamlfind query lablgtkosx 2> /dev/null);
-        then
-            IDEARCHFLAGS=lablgtkosx.cmxa
-	    IDEARCHDEF=QUARTZ
-	elif [ "$ARCH" = "win32" ];
-        then
-	    IDEARCHFLAGS=
-	    IDEARCHFILE=ide/ide_win32_stubs.o
-	    IDEARCHDEF=WIN32
-	fi
-    fi
-fi
-
-case $COQIDE in
-    byte|opt)
-        LABLGTKINCLUDES="-I $LABLGTKLIB";;
-    no)
-        LABLGTKINCLUDES="";;
-esac
-
-[ x$lablgtkosxdir = x ] || LABLGTKINCLUDES="$LABLGTKINCLUDES -I $lablgtkosxdir"
-
-# strip command
-
-case $ARCH in
-    Darwin) if [ "$HASNATDYNLINK" = "true" ]
-	then
-	  STRIPCOMMAND="true"
-	else
-	  STRIPCOMMAND="strip"
-	fi;;
-    *)
-    if [ "$coq_profile_flag" = "-p" ] || [ "$coq_debug_flag" = "-g" ]
-    then
-	STRIPCOMMAND="true"
-    else
-	STRIPCOMMAND="strip"
-    fi
-esac
-
-### Test if documentation can be compiled (latex, hevea)
-
-if test "$with_doc" = "all" 
-then
-    for cmd in "latex" "hevea" ; do
-	if test ! -x "`which $cmd`"
-	then 
-	    echo "$cmd was not found; documentation will not be available"
-	    with_doc=no
-	    break
-	fi
-    done
-fi
-
-###########################################
-# bindir, libdir, mandir, docdir, etc.
-
-# OCaml only understand Windows filenames (C:\...)
-case $ARCH in
-    win32) COQSRC=`mk_win_path "$COQSRC"`
-	   CAMLBIN=`mk_win_path "$CAMLBIN"`
-	   CAMLP4BIN=`mk_win_path "$CAMLP4BIN"`
-esac
-
-case $src_spec in
-  no) COQTOP=${COQSRC}
-esac
-
-case $ARCH$CYGWIN in
-  win32)
-	 W32PREF='C:\coq\'
-	 bindir_def="${W32PREF}bin"
-	 libdir_def="${W32PREF}lib"
-	 configdir_def="${W32PREF}config"
-	 datadir_def="${W32PREF}share"
-	 mandir_def="${W32PREF}man"
-	 docdir_def="${W32PREF}doc"
-	 emacslib_def="${W32PREF}emacs"
-	 coqdocdir_def="${W32PREF}latex";;
-  *)
-	 bindir_def=/usr/local/bin
-	 libdir_def=/usr/local/lib/coq
-	 configdir_def=/etc/xdg/coq
-	 datadir_def=/usr/local/share/coq
-	 mandir_def=/usr/local/share/man
-	 docdir_def=/usr/local/share/doc/coq
-	 emacslib_def=/usr/local/share/emacs/site-lisp
-	 coqdocdir_def=/usr/local/share/texmf/tex/latex/misc;;
-esac
-
-emacs_def=emacs
-
-case $bindir_spec/$prefix_spec/$local in
-    yes/*/*) BINDIR=$bindir ;;
-    */yes/*) BINDIR=$prefix/bin ;;
-    */*/true) BINDIR=$COQTOP/bin ;;
-    *)  printf "Where should I install the Coq binaries [%s]? " "$bindir_def"
-        read BINDIR
-	case $BINDIR in
-	    "") BINDIR=$bindir_def;;
-	    *) true;;
-	esac;;
-esac
-
-case $libdir_spec/$prefix_spec/$local in
-    yes/*/*) LIBDIR=$libdir;;
-    */yes/*)
-        libdir_spec=yes
-        case $ARCH in
-          win32) LIBDIR=$prefix ;;
-          *)  LIBDIR=$prefix/lib/coq ;;
-        esac ;;
-    */*/true) LIBDIR=$COQTOP ;;
-    *)  printf "Where should I install the Coq library [%s]? " "$libdir_def"
-        read LIBDIR
-        libdir_spec=yes
-	case $LIBDIR in
-	    "") LIBDIR=$libdir_def;;
-	    *) true;;
-	esac;;
-esac
-
-case $configdir_spec/$prefix_spec/$local in
-    yes/*/*) CONFIGDIR=$configdir;;
-    */yes/*) configdir_spec=yes
-	case $ARCH in
-	    win32) CONFIGDIR=$prefix/config;;
-            *) CONFIGDIR=$prefix/etc/xdg/coq;;
-	esac;;
-    */*/true) CONFIGDIR=$COQTOP/ide
-    configdir_spec=yes;;
-    *)  printf "Where should I install the Coqide configuration files [%s]? " "$configdir_def"
-        read CONFIGDIR
-	case $CONFIGDIR in
-	    "") CONFIGDIR=$configdir_def;;
-	    *) configdir_spec=yes;;
-	esac;;
-esac
-
-case $datadir_spec/$prefix_spec/$local in
-    yes/*/*) DATADIR=$datadir;;
-    */yes/*) DATADIR=$prefix/share/coq;;
-    */*/true) DATADIR=$COQTOP/ide
-        datadir_spec=yes;;
-    *)  printf "Where should I install the Coqide data files [%s]? " "$datadir_def"
-        read DATADIR
-	case $DATADIR in
-	    "") DATADIR=$datadir_def;;
-	    *) datadir_spec=yes;;
-	esac;;
-esac
-
-case $mandir_spec/$prefix_spec/$local in
-    yes/*/*) MANDIR=$mandir;;
-    */yes/*) MANDIR=$prefix/share/man ;;
-    */*/true) MANDIR=$COQTOP/man ;;
-    *)  printf "Where should I install the Coq man pages [%s]? "  "$mandir_def"
-        read MANDIR
-	case $MANDIR in
-	    "") MANDIR=$mandir_def;;
-	    *) true;;
-	esac;;
-esac
-
-case $docdir_spec/$prefix_spec/$local in
-    yes/*/*) DOCDIR=$docdir;;
-    */yes/*) DOCDIR=$prefix/share/doc/coq;;
-    */*/true) DOCDIR=$COQTOP/doc;;
-    *)  printf "Where should I install the Coq documentation [%s]? " "$docdir_def"
-        read DOCDIR
-	case $DOCDIR in
-	    "") DOCDIR=$docdir_def;;
-	    *) true;;
-	esac;;
-esac
-
-case $emacslib_spec/$prefix_spec/$local in
-    yes/*/*) EMACSLIB=$emacslib;;
-    */yes/*)
-        case $ARCH in
-          win32) EMACSLIB=$prefix/emacs ;;
-          *)  EMACSLIB=$prefix/share/emacs/site-lisp ;;
-        esac ;;
-    */*/true) EMACSLIB=$COQTOP/tools/emacs ;;
-    *)  printf "Where should I install the Coq Emacs mode [%s]? " "$emacslib_def"
-        read EMACSLIB
-	case $EMACSLIB in
-	    "") EMACSLIB=$emacslib_def;;
-	    *) true;;
-	esac;;
-esac
-
-case $coqdocdir_spec/$prefix_spec/$local in
-    yes/*/*) COQDOCDIR=$coqdocdir;;
-    */yes/*)
-        case $ARCH in
-          win32) COQDOCDIR=$prefix/latex ;;
-          *)  COQDOCDIR=$prefix/share/emacs/site-lisp ;;
-        esac ;;
-    */*/true) COQDOCDIR=$COQTOP/tools/coqdoc ;;
-    *)  printf "Where should I install Coqdoc TeX/LaTeX files [%s]? " "$coqdocdir_def"
-        read COQDOCDIR
-	case $COQDOCDIR in
-	    "") COQDOCDIR=$coqdocdir_def;;
-	    *) true;;
-	esac;;
-esac
-
-# Determine if we enable -custom by default (Windows and MacOS)
-CUSTOM_OS=no
-if [ "$ARCH" = "win32" ] || [ "$ARCH" = "Darwin" ]; then
-    CUSTOM_OS=yes
-fi
-
-BUILDLDPATH="# you might want to set CAML_LD_LIBRARY_PATH by hand!"
-case $coqrunbyteflags_spec/$local/$custom_spec/$CUSTOM_OS in
-    yes/*/*/*) COQRUNBYTEFLAGS="$coqrunbyteflags";;
-    */*/yes/*|*/*/*/yes) COQRUNBYTEFLAGS="-custom";;
-    */true/*/*) COQRUNBYTEFLAGS="-dllib -lcoqrun -dllpath '$COQTOP'/kernel/byterun";;
-    *)
-        COQRUNBYTEFLAGS="-dllib -lcoqrun -dllpath '$LIBDIR'"
-        BUILDLDPATH="export CAML_LD_LIBRARY_PATH='$COQTOP'/kernel/byterun:$CAML_LD_LIBRARY_PATH";;
-esac
-case $coqtoolsbyteflags_spec/$custom_spec/$CUSTOM_OS in
-    yes/*/*) COQTOOLSBYTEFLAGS="$coqtoolsbyteflags";;
-    */yes/*|*/*/yes) COQTOOLSBYTEFLAGS="-custom";;
-    *) COQTOOLSBYTEFLAGS="";;
-esac
-
-# case $emacs_spec in
-#     no) printf "Which Emacs command should I use to compile coq.el [%s]? " "$emacs_def"
-#         read EMACS
-	
-# 	case $EMACS in
-# 	    "") EMACS="$emacs_def";;
-# 	    *) true;;
-# 	esac;;
-#     yes) EMACS="$emacs";;
-# esac
-
-
-
-###########################################
-# Summary of the configuration
-
-echo ""
-echo "  Coq top directory                 : $COQTOP"
-echo "  Architecture                      : $ARCH"
-if test ! -z "$OS" ; then
-  echo "  Operating system                  : $OS"
-fi
-echo "  Coq VM bytecode link flags        : $COQRUNBYTEFLAGS"
-echo "  Coq tools bytecode link flags     : $COQTOOLSBYTEFLAGS"
-echo "  OS dependent libraries            : $OSDEPLIBS"
-echo "  Objective-Caml/Camlp4 version     : $CAMLVERSION"
-echo "  Objective-Caml/Camlp4 binaries in : $CAMLBIN"
-echo "  Objective-Caml library in         : $CAMLLIB"
-echo "  Camlp4 library in                 : $CAMLP4LIB"
-if test "$best_compiler" = opt ; then
-echo "  Native dynamic link support       : $HASNATDYNLINK"
-fi
-if test "$COQIDE" != "no"; then
-echo "  Lablgtk2 library in               : $LABLGTKLIB"
-fi
-if test "$IDEARCHDEF" = "QUARTZ"; then
-echo "  Mac OS integration is on"
-fi
-if test "$with_doc" = "all"; then
-echo "  Documentation                     : All"
-else
-echo "  Documentation                     : None"
-fi
-echo "  CoqIde                            : $COQIDE"
-echo "  Web browser                       : $BROWSER"
-echo "  Coq web site                      : $WWWCOQ"
-echo ""
-
-echo "  Paths for true installation:"
-echo "    binaries      will be copied in $BINDIR"
-echo "    library       will be copied in $LIBDIR"
-echo "    config files  will be copied in $CONFIGDIR"
-echo "    data files    will be copied in $DATADIR"
-echo "    man pages     will be copied in $MANDIR"
-echo "    documentation will be copied in $DOCDIR"
-echo "    emacs mode    will be copied in $EMACSLIB"
-echo ""
-
-##################################################
-# Building the $COQTOP/dev/ocamldebug-coq file
-##################################################
-
-OCAMLDEBUGCOQ=$COQSRC/dev/ocamldebug-coq
-
-if test "$coq_debug_flag" = "-g" ; then
-  rm -f $OCAMLDEBUGCOQ
-  sed -e "s|COQTOPDIRECTORY|$COQTOP|" \
-      -e "s|COQLIBDIRECTORY|$LIBDIR|" \
-      -e "s|CAMLBINDIRECTORY|$CAMLBIN|" \
-      -e "s|CAMLP4LIBDIRECTORY|$FULLCAMLP4LIB|"\
-      $OCAMLDEBUGCOQ.template > $OCAMLDEBUGCOQ
-  chmod a-w,a+x $OCAMLDEBUGCOQ
-fi
-
-####################################################
-# Fixing lablgtk types (before/after 2.6.0) 
-####################################################
-
-if [ ! "$COQIDE" = "no" ]; then 
-    if grep "class view " "$lablgtkdir/gText.mli" | grep -q "\[>" ; then
-       if grep -q "?accepts_tab:bool" "$lablgtkdir/gText.mli" ; then
-        cp -f ide/undo_lablgtk_ge212.mli ide/undo.mli
-       else
-	cp -f ide/undo_lablgtk_ge26.mli ide/undo.mli
-       fi
-    else
-	cp -f ide/undo_lablgtk_lt26.mli ide/undo.mli
-    fi
-fi  
-
-##############################################
-# Creation of configuration files
-##############################################
-
-mlconfig_file="$COQSRC/config/coq_config.ml"
-config_file="$COQSRC/config/Makefile"
-config_template="$COQSRC/config/Makefile.template"
-
-
-### Warning !!
-### After this line, be careful when using variables,
-### since some of them (e.g. $COQSRC) will be escaped
-
-escape_string () {
-    "$ocamlexec" "tools/escape_string.ml" "$1"
-}
-
-# Escaped version of browser command
-BROWSER=`escape_string "$BROWSER"`
-
-# Under Windows, we now escape the backslashes that will ends in
-# ocaml strings (coq_config.ml) or in Makefile variables.
-
-case $ARCH in
-    win32)
-	COQTOP=`escape_string "$COQTOP"`
-	BINDIR=`escape_string "$BINDIR"`
-	COQSRC=`escape_string "$COQSRC"`
-	LIBDIR=`escape_string "$LIBDIR"`
-	CONFIGDIR=`escape_string "$CONFIGDIR"`
-	DATADIR=`escape_string "$DATADIR"`
-	CAMLBIN=`escape_string "$CAMLBIN"`
-	CAMLLIB=`escape_string "$CAMLLIB"`
-	MANDIR=`escape_string "$MANDIR"`
-	DOCDIR=`escape_string "$DOCDIR"`
-	EMACSLIB=`escape_string "$EMACSLIB"`
-	COQDOCDIR=`escape_string "$COQDOCDIR"`
-	CAMLP4BIN=`escape_string "$CAMLP4BIN"`
-	CAMLP4LIB=`escape_string "$CAMLP4LIB"`
-	LABLGTKINCLUDES=`escape_string "$LABLGTKINCLUDES"`
-	COQRUNBYTEFLAGS=`escape_string "$COQRUNBYTEFLAGS"`
-	COQTOOLSBYTEFLAGS=`escape_string "$COQTOOLSBYTEFLAGS"`
-	BUILDLDPATH=`escape_string "$BUILDLDPATH"`
-	ocamlexec=`escape_string "$ocamlexec"`
-	bytecamlc=`escape_string "$bytecamlc"`
-	nativecamlc=`escape_string "$nativecamlc"`
-	ocamlmklibexec=`escape_string "$ocamlmklibexec"`
-	ocamldepexec=`escape_string "$ocamldepexec"`
-	ocamldocexec=`escape_string "$ocamldocexec"`
-	ocamllexexec=`escape_string "$ocamllexexec"`
-	ocamlyaccexec=`escape_string "$ocamlyaccexec"`
-	camlp4oexec=`escape_string "$camlp4oexec"`
-    ;;
-esac
-
-case $libdir_spec in
-    yes) LIBDIR_OPTION="Some \"$LIBDIR\"";;
-    *) LIBDIR_OPTION="None";;
-esac
-
-case $configdir_spec in
-    yes) CONFIGDIR_OPTION="Some \"$CONFIGDIR\"";;
-    *) CONFIGDIR_OPTION="None";;
-esac
-
-case $datadir_spec in
-    yes) DATADIR_OPTION="Some \"$DATADIR\"";;
-    *) DATADIR_OPTION="None";;
-esac
-
-#####################################################
-# Building the $COQTOP/config/coq_config.ml file
-#####################################################
+## Parse the args, only looking for -camldir
+## We avoid using shift to keep "$@" intact
 
-rm -f "$mlconfig_file"
-cat << END_OF_COQ_CONFIG > $mlconfig_file
-(* DO NOT EDIT THIS FILE: automatically generated by ../configure *)
-
-let local = $local
-let coqrunbyteflags = "$COQRUNBYTEFLAGS"
-let coqlib = $LIBDIR_OPTION
-let configdir = $CONFIGDIR_OPTION
-let datadir = $DATADIR_OPTION
-let docdir = "$DOCDIR"
-let ocaml = "$ocamlexec"
-let ocamlc = "$bytecamlc"
-let ocamlopt = "$nativecamlc"
-let ocamlmklib = "$ocamlmklibexec"
-let ocamldep = "$ocamldepexec"
-let ocamldoc = "$ocamldocexec"
-let ocamlyacc = "$ocamlyaccexec"
-let ocamllex = "$ocamllexexec"
-let camlbin = "$CAMLBIN"
-let camllib = "$CAMLLIB"
-let camlp4 = "$CAMLP4"
-let camlp4o = "$camlp4oexec"
-let camlp4bin = "$CAMLP4BIN"
-let camlp4lib = "$CAMLP4LIB"
-let camlp4compat = "$CAMLP4COMPAT"
-let coqideincl = "$LABLGTKINCLUDES"
-let cflags = "$cflags"
-let best = "$best_compiler"
-let arch = "$ARCH"
-let has_coqide = "$COQIDE"
-let gtk_platform = \`$IDEARCHDEF
-let has_natdynlink = $HASNATDYNLINK
-let natdynlinkflag = "$NATDYNLINKFLAG"
-let osdeplibs = "$OSDEPLIBS"
-let version = "$VERSION"
-let caml_version = "$CAMLVERSION"
-let date = "$DATE"
-let compile_date = "$COMPILEDATE"
-let vo_magic_number = $VOMAGIC
-let state_magic_number = $STATEMAGIC
-let exec_extension = "$EXE"
-let with_geoproof = ref $with_geoproof
-let browser = "$BROWSER"
-let wwwcoq = "$WWWCOQ"
-let wwwrefman = wwwcoq ^ "distrib/" ^ version ^ "/refman/"
-let wwwstdlib = wwwcoq ^ "distrib/" ^ version ^ "/stdlib/"
-let localwwwrefman = "file:/" ^ docdir ^ "html/refman"
-
-END_OF_COQ_CONFIG
-
-# to be sure printf is found on windows when spaces occur in PATH variable
-PRINTF=`which printf`
-
-# Subdirectories of theories/ added in coq_config.ml
-subdirs () {
-    (cd $1; find * \( -name .svn -prune \) -o \( -type d -exec $PRINTF "\"%s\";\n" {} \; \) >> "$mlconfig_file")
-}
-
-echo "let theories_dirs = [" >> "$mlconfig_file"
-subdirs theories
-echo "]" >> "$mlconfig_file"
-
-echo "let plugins_dirs = [" >> "$mlconfig_file"
-subdirs plugins
-echo "]" >> "$mlconfig_file"
-
-chmod a-w "$mlconfig_file"
-
-
-###############################################
-# Building the $COQTOP/config/Makefile file
-###############################################
-
-rm -f "$config_file"
-cat << END_OF_MAKEFILE > $config_file
-###### config/Makefile : Configuration file for Coq ##############
-#                                                                #
-# This file is generated by the script "configure"               #
-# DO NOT EDIT IT !! DO NOT EDIT IT !! DO NOT EDIT IT !!          #
-# If something is wrong below, then rerun the script "configure" #
-# with the good options (see the file INSTALL).                  #
-#                                                                #
-##################################################################
-
-#Variable used to detect whether ./configure has run successfully.
-COQ_CONFIGURED=yes
-
-# Local use (no installation)
-LOCAL=$local
-
-# Bytecode link flags for VM ("-custom" or "-dllib -lcoqrun")
-COQRUNBYTEFLAGS=$COQRUNBYTEFLAGS
-COQTOOLSBYTEFLAGS=$COQTOOLSBYTEFLAGS
-$BUILDLDPATH
-
-# Paths for true installation
-# BINDIR=path where coqtop, coqc, coqmktop, coq-tex, coqdep, gallina and
-#        do_Makefile will reside
-# LIBDIR=path where the Coq library will reside
-# MANDIR=path where to install manual pages
-# EMACSDIR=path where to put Coq's Emacs mode (coq.el)
-BINDIR="$BINDIR"
-COQLIBINSTALL="$LIBDIR"
-CONFIGDIR="$CONFIGDIR"
-DATADIR="$DATADIR"
-MANDIR="$MANDIR"
-DOCDIR="$DOCDIR"
-EMACSLIB="$EMACSLIB"
-EMACS=$EMACS
-
-# Path to Coq distribution
-COQSRC="$COQSRC"
-VERSION=$VERSION
-
-# Ocaml version number
-CAMLVERSION=$CAMLTAG
-
-# Ocaml libraries
-CAMLLIB="$CAMLLIB"
-
-# Ocaml .h directory
-CAMLHLIB="$CAMLLIB"
-
-# Camlp4 : flavor, binaries, libraries ...
-# NB : CAMLP4BIN can be empty if camlp4 is in the PATH
-# NB : avoid using CAMLP4LIB (conflict under Windows)
-CAMLP4BIN="$CAMLP4BIN"
-CAMLP4=$CAMLP4
-CAMLP4O=$camlp4oexec
-CAMLP4COMPAT=$CAMLP4COMPAT
-MYCAMLP4LIB="$CAMLP4LIB"
-
-# LablGTK
-COQIDEINCLUDES=$LABLGTKINCLUDES
-
-# Objective-Caml compile command
-OCAML="$ocamlexec"
-OCAMLC="$bytecamlc"
-OCAMLMKLIB="$ocamlmklibexec"
-OCAMLOPT="$nativecamlc"
-OCAMLDEP="$ocamldepexec"
-OCAMLDOC="$ocamldocexec"
-OCAMLLEX="$ocamllexexec"
-OCAMLYACC="$ocamlyaccexec"
-
-# Caml link command and Caml make top command
-CAMLLINK="$bytecamlc"
-CAMLOPTLINK="$nativecamlc"
-CAMLMKTOP="$ocamlmktopexec"
-
-# Caml flags
-CAMLFLAGS=-rectypes $coq_annotate_flag
-
-# Compilation debug flags
-CAMLDEBUG=$coq_debug_flag
-CAMLDEBUGOPT=$coq_debug_flag_opt
-
-# User compilation flag
-USERFLAGS=
-
-# Flags for GCC
-CFLAGS=$cflags
-
-# Compilation profile flag
-CAMLTIMEPROF=$coq_profile_flag
-
-# The best compiler: native (=opt) or bytecode (=byte) if no native compiler
-BEST=$best_compiler
-
-# Your architecture
-# Can be obtain by UNIX command arch
-ARCH=$ARCH
-HASNATDYNLINK=$NATDYNLINKFLAG
-
-# Supplementary libs for some systems, currently:
-#  . Sun Solaris: -cclib -lunix -cclib -lnsl -cclib -lsocket
-#  . others     : -cclib -lunix
-OSDEPLIBS=$OSDEPLIBS
-
-# executable files extension, currently:
-#  Unix systems:
-#  Win32 systems : .exe
-EXE=$EXE
-DLLEXT=$DLLEXT
-
-# the command MKDIR (try to replace it with mkdirhier if you have problems)
-MKDIR=mkdir -p
-
-# where to put the coqdoc.sty style file
-COQDOCDIR="$COQDOCDIR"
-
-#the command STRIP
-# Unix systems and profiling: true
-# Unix systems and no profiling: strip
-STRIP=$STRIPCOMMAND
-
-# CoqIde (no/byte/opt)
-HASCOQIDE=$COQIDE
-IDEOPTFLAGS=$IDEARCHFLAGS
-IDEOPTDEPS=$IDEARCHFILE
-IDEOPTINT=$IDEARCHDEF
-
-# Defining REVISION
-CHECKEDOUT=$checkedout
-
-# Option to control compilation and installation of the documentation
-WITHDOC=$with_doc
-
-# make or sed are bogus and believe lines not terminating by a return
-# are inexistent
-END_OF_MAKEFILE
+last=
+for i; do
+   case $last in
+       -camldir|--camldir) cmd="$i/ocaml"; break;;
+   esac
+   last=$i
+done
 
-chmod a-w "$config_file"
+## We check that $cmd is ok before the real exec $cmd
 
-##################################################
-# The end
-####################################################
+`$cmd -version > /dev/null 2>&1` && exec $cmd $script "$@"
 
-echo "If anything in the above is wrong, please restart './configure'."
-echo
-echo "*Warning* To compile the system for a new architecture"
-echo "          don't forget to do a 'make archclean' before './configure'."
+## If we're still here, something is wrong with $cmd
 
+echo "Error: failed to run $cmd"
+echo "Please use the option -camldir <dir> if 'ocaml' is installed"
+echo "in directory <dir>, or add <dir> to your path."
+echo "Configuration script failed!"
+exit 1