pour win32

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5270 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 73 insertions, 60 deletions

diff --git a/configure b/configure
index 689cd4804..162f0cb78 100755
--- a/configure
+++ b/configure
@@ -125,7 +125,7 @@ case $arch_spec in
 	    ARCH=`/usr/ucb/arch`
 	elif test -x /bin/uname && (/bin/uname -s | grep -q -i CYGWIN) ; then
 	    ARCH=win32
-	    # cygwin returns a name of the form \\cygdrive\\c\\... 
+	    # cygwin returns a name of the form /cygdrive/c/... 
 	    # that coqc does not understand; need to transform it
 	    COQTOP=`echo $COQTOP | sed -e "s#.*cygdrive.\(.\)#\1:#"`
 	elif test -x /usr/bin/uname ; then
@@ -143,10 +143,10 @@ esac
 
 case $ARCH in
   win32)
-	 bindir_def=\\coq\\bin
-	 libdir_def=\\coq\\lib
-	 mandir_def=\\coq\\man
-	 emacslib_def=\\coq\\emacs;;
+	 bindir_def=C:\\coq\\bin
+	 libdir_def=C:\\coq\\lib
+	 mandir_def=C:\\coq\\man
+	 emacslib_def=C:\\coq\\emacs;;
   *)
 	 bindir_def=/usr/local/bin
 	 libdir_def=/usr/local/lib/coq
@@ -341,9 +341,9 @@ fi
 
 # Tell on windows if ocaml understands cygwin or windows path formats
 
-"$CAMLC" -o config/giveostype config/giveostype.ml
-CAMLOSTYPE=`config/giveostype`
-rm config/giveostype
+#"$CAMLC" -o config/giveostype config/giveostype.ml
+#CAMLOSTYPE=`config/giveostype`
+#rm config/giveostype
 
 case $ARCH in
     win32)
@@ -385,16 +385,75 @@ echo "    man pages  will be copied in $MANDIR"
 echo "    emacs mode will be copied in $EMACSLIB"
 echo ""
 
+#####################################################
+# Building the $COQTOP/config/coq_config.ml file
+#####################################################
+
+# damned backslashes under M$Windows
+case $ARCH in
+    win32)
+	CAMLLIB=`echo $CAMLLIB |sed -e 's|\\\|\\\\\\\|g'`
+	BINDIR=`echo $BINDIR |sed -e 's|\\\|\\\\\\\|g'`
+	LIBDIR=`echo $LIBDIR |sed -e 's|\\\|\\\\\\\|g'`
+  	MANDIR=`echo $MANDIR |sed -e 's|\\\|\\\\\\\|g'`
+   	EMACSLIB=`echo $EMACSLIB |sed -e 's|\\\|\\\\\\\|g'`
+	;;
+esac
+
+mlconfig_file=$COQTOP/config/coq_config.ml
+rm -f $mlconfig_file
+cat << END_OF_COQ_CONFIG > $mlconfig_file
+(* DO NOT EDIT THIS FILE: automatically generated by ../configure *)
+
+let local = $local
+let bindir = "$BINDIR" 
+let coqlib = "$LIBDIR"
+let coqtop = "$COQTOP"
+let camllib = "$CAMLLIB"
+let camlp4lib = "$CAMLP4LIB"
+let best = "$best_compiler"
+let arch = "$ARCH"
+let osdeplibs = "$OSDEPLIBS"
+let version = "$VERSION"
+let versionsi = "$VERSIONSI"
+let date = "$DATE"
+let compile_date = "$COMPILEDATE"
+let exec_extension = "$EXE"
+
+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 * -type d ! -name CVS -exec $PRINTF "\"%s\";\n" {} \; | grep -v extraction/test | grep -v correctness >> $mlconfig_file)
+}
+
+echo "let theories_dirs = [" >> $mlconfig_file
+subdirs theories
+echo "]" >> $mlconfig_file
+
+echo "let contrib_dirs = [" >> $mlconfig_file
+subdirs contrib
+echo "]" >> $mlconfig_file
+
+chmod a-w $mlconfig_file
+
+
+###############################################
 # Building the $COQTOP/config/Makefile file
+###############################################
 
 rm -f $COQTOP/config/Makefile
 
+# damned backslashes under M$Windows (bis)
 case $ARCH in
     win32)
-	BINDIR=`echo $BINDIR |sed -e 's|\\\|/|g'`
-	LIBDIR=`echo $LIBDIR |sed -e 's|\\\|/|g'`
-  	MANDIR=`echo $MANDIR |sed -e 's|\\\|/|g'`
-   	EMACSLIB=`echo $EMACSLIB |sed -e 's|\\\|/|g'`
+	BINDIR=`echo $BINDIR |sed -e 's|\\\|\\\\\\\|g'`
+	LIBDIR=`echo $LIBDIR |sed -e 's|\\\|\\\\\\\|g'`
+  	MANDIR=`echo $MANDIR |sed -e 's|\\\|\\\\\\\|g'`
+   	EMACSLIB=`echo $EMACSLIB |sed -e 's|\\\|\\\\\\\|g'`
 	;;
 esac
 
@@ -426,7 +485,9 @@ sed -e "s|LOCALINSTALLATION|$local|" \
 
 chmod a-w $COQTOP/config/Makefile
 
+##################################################
 # Building the $COQTOP/dev/ocamldebug-v7 file
+####################################################
 
 if test "$coq_debug_flag" = "-g" ; then
   rm -f $COQTOP/dev/ocamldebug-v7
@@ -443,54 +504,6 @@ if test "$coq_debug_flag" = "-g" ; then
   chmod a-w,a+x $COQTOP/dev/ocamldebug-v7
 fi
 
-# Building the $COQTOP/config/coq_config.ml file
-
-mlconfig_file=$COQTOP/config/coq_config.ml
-rm -f $mlconfig_file
-cat << END_OF_COQ_CONFIG > $mlconfig_file
-(* DO NOT EDIT THIS FILE: automatically generated by ../configure *)
-
-let local = $local
-let bindir = "$BINDIR" 
-let coqlib = "$LIBDIR"
-let coqtop = "$COQTOP"
-let camllib = "$CAMLLIB"
-let camlp4lib = "$CAMLP4LIB"
-let best = "$best_compiler"
-let arch = "$ARCH"
-let osdeplibs = "$OSDEPLIBS"
-let version = "$VERSION"
-let versionsi = "$VERSIONSI"
-let date = "$DATE"
-let compile_date = "$COMPILEDATE"
-let exec_extension = "$EXE"
-
-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 * -type d ! -name CVS -exec $PRINTF "\"%s\";\n" {} \; | grep -v extraction/test | grep -v correctness >> $mlconfig_file)
-}
-
-echo "let theories_dirs = [" >> $mlconfig_file
-subdirs theories
-echo "]" >> $mlconfig_file
-
-echo "let contrib_dirs = [" >> $mlconfig_file
-subdirs contrib
-echo "]" >> $mlconfig_file
-
-if test "$CAMLOSTYPE" = "Win32" ; then
-# We change: / -> \\ and \ -> \\ (dos paths)
-# This is a bit tricky
-sed -e "s|\\\\\\\\\\\\\\\|\\\|" -e "s|/|\\\|g"  -e "s|\\\|\\\\\\\|g" $mlconfig_file > $mlconfig_file.win
-mv $mlconfig_file.win $mlconfig_file
-fi
-chmod a-w $mlconfig_file
-
 echo "If anything in the above is wrong, please restart './configure'"
 echo
 echo "*Warning* To compile the system for a new architecture"