Imported Upstream version 8.0pl3+8.1betaupstream/8.0pl3+8.1beta

1 files changed, 36 insertions, 8 deletions

diff --git a/configure b/configure
index a380cf86..f2bb36b9 100755
--- a/configure
+++ b/configure
@@ -6,8 +6,8 @@
 # 
 ##################################
 
-VERSION=8.1-alpha
-DATE="Mar 2006"
+VERSION=8.1beta
+DATE="Jun 2006"
 
 # a local which command for sh
 which () {
@@ -36,10 +36,13 @@ mandir_spec=no
 emacslib_spec=no
 emacs_spec=no
 coqdocdir_spec=no
+fsets_opt=no
+fsets=all
 reals_opt=no
 reals=all
 arch_spec=no
 coqide_spec=no
+with_geoproof=true
 
 COQTOP=`pwd`
 
@@ -69,6 +72,8 @@ while : ; do
 		    emacslib=$COQTOP/tools/emacs
 		    coqdocdir_spec=yes
 		    coqdocdir=$COQTOP/tools/coqdoc
+		    fsets_opt=yes
+		    fsets=all
 		    reals_opt=yes
 		    reals=all;;
     -src|--src) COQTOP=$2
@@ -97,12 +102,21 @@ while : ; do
     -opt|--opt) bytecamlc=ocamlc.opt
                 camlp4o=camlp4o  # can't add .opt since dyn load'll be required
                 nativecamlc=ocamlopt.opt;;
+    -fsets|--fsets) fsets_opt=yes
+                    fsets=$2
+		    shift;;
     -reals|--reals) reals_opt=yes
 		    reals=$2
 		    shift;;
     -coqide|--coqide) coqide_spec=yes
 		      COQIDE=$2
 		      shift;;
+    -with-geoproof|--with-geoproof) 
+	  case $2 in
+	      yes) with_geoproof=true;;
+	      no) with_geoproof=false;;
+	  esac
+	  shift;;
     -byte-only|-byteonly|--byteonly|--byte-only) best_compiler=byte;;
     -debug|--debug) coq_debug_flag=-g;;
     -profile|--profile) coq_profile_flag=-p;;
@@ -219,6 +233,18 @@ case $coqdocdir_spec in
     yes) COQDOCDIR=$coqdocdir;;
 esac
 
+case $fsets_opt in
+    no) echo "Should I compile the complete theory of finite sets [Y/N, default is Y] ?"
+	read fsets_ans
+
+	case $fsets_ans in
+	    "N"|"n"|"No"|"NO"|"no")
+		    fsets=basic;;
+		*) fsets=all;;
+	esac;;
+    yes) true;;
+esac
+
 case $reals_opt in
     no) echo "Should I compile the complete theory of real analysis [Y/N, default is Y] ?"
 	read reals_ans
@@ -410,6 +436,11 @@ 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 "$fsets" = "all"; then
+echo "  FSets theory                      : All"
+else
+echo "  FSets theory                      : Basic"
+fi
 if test "$reals" = "all"; then
 echo "  Reals theory                      : All"
 else
@@ -459,6 +490,7 @@ let versionsi = "$VERSIONSI"
 let date = "$DATE"
 let compile_date = "$COMPILEDATE"
 let exec_extension = "$EXE"
+let with_geoproof = ref $with_geoproof
 
 END_OF_COQ_CONFIG
 
@@ -523,6 +555,7 @@ sed -e "s|LOCALINSTALLATION|$local|" \
     -e "s|BYTECAMLC|$bytecamlc|" \
     -e "s|NATIVECAMLC|$nativecamlc|" \
     -e "s|STRIPCOMMAND|$STRIPCOMMAND|" \
+    -e "s|FSETSOPT|$fsets|" \
     -e "s|REALSOPT|$reals|" \
     -e "s|COQIDEOPT|$COQIDE|" \
       $COQTOP/config/Makefile.template > $COQTOP/config/Makefile
@@ -550,11 +583,6 @@ if test "$coq_debug_flag" = "-g" ; then
   chmod a-w,a+x $OCAMLDEBUGCOQ
 fi
 
-# Compatibility with previous name
-if [ ! -f $COQTOP/dev/ocamldebug-v7 ] ; then
-  ln -s `basename $OCAMLDEBUGCOQ` $COQTOP/dev/ocamldebug-v7
-fi
-
 ##################################################
 # Fixing lablgtk types
 ####################################################
@@ -574,4 +602,4 @@ echo
 echo "*Warning* To compile the system for a new architecture"
 echo "          don't forget to do a 'make archclean' before './configure'."
 
-# $Id: configure 8712 2006-04-14 10:34:47Z notin $
+# $Id: configure 8932 2006-06-09 09:29:03Z notin $