Modification du configure pour paramétrer les exécutables liés à la compilation C

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

3 files changed, 27 insertions, 6 deletions

diff --git a/Makefile b/Makefile
index 44440ad27..b71c7c5aa 100644
--- a/Makefile
+++ b/Makefile
@@ -346,9 +346,6 @@ OBJSCMO=$(CONFIG) $(LIBREP) $(KERNEL) $(LIBRARY) $(PRETYPING) $(INTERP) \
 ###########################################################################
 
 CINCLUDES= -I $(CAMLHLIB)
-CC=gcc
-AR=ar
-RANLIB=ranlib
 
 ifeq ($(CAMLVERSION),OCAML307)
   CFLAGS=-fno-defer-pop -Wall -Wno-unused -DOCAML_307
@@ -1724,8 +1721,8 @@ depend: beforedepend dependp4 ml4filesml
 	  echo `$(CAMLP4DEPS) $$f` >> .depend; \
 	done
 # 5.  We express dependencies of .o files
-	gcc -MM $(CINCLUDES) kernel/byterun/*.c >> .depend
-	gcc -MM  $(CINCLUDES) kernel/byterun/*.c | sed -e 's/\.o/.d.o/' >> \
+	$(CC) -MM $(CINCLUDES) kernel/byterun/*.c >> .depend
+	$(CC) -MM  $(CINCLUDES) kernel/byterun/*.c | sed -e 's/\.o/.d.o/' >> \
                     .depend
 # 6. Finally, we erase the generated .ml files
 	rm -f $(ML4FILESML)
diff --git a/config/Makefile.template b/config/Makefile.template
index 030670340..4e592e6e6 100644
--- a/config/Makefile.template
+++ b/config/Makefile.template
@@ -81,6 +81,11 @@ P4DEP=$(COQTOP)/bin/$(ARCH)/camlp4dep
 # Can be obtain by UNIX command arch
 ARCH=ARCHITECTURE
 
+# Your C compiler and co
+CC="CCEXEC"
+AR="AREXEC"
+RANLIB="RANLIBEXEC"
+
 # Supplementary libs for some systems, currently:
 #  . Sun Solaris: -cclib -lunix -cclib -lnsl -cclib -lsocket
 #  . others     : -cclib -lunix
diff --git a/configure b/configure
index 7a9e10de4..641e298f5 100755
--- a/configure
+++ b/configure
@@ -29,6 +29,10 @@ coq_debug_flag=
 coq_profile_flag=
 best_compiler=opt
 
+gcc_exec=gcc
+ar_exec=ar
+ranlib_exec=ranlib
+
 local=false
 src_spec=no
 prefix_spec=no
@@ -106,10 +110,22 @@ while : ; do
 	      no) with_geoproof=false;;
 	  esac
 	  shift;;
+    -with-cc|-with-gcc|--with-cc|--with-gcc) 
+	  gcc_spec=yes
+	  gcc_exec=$2
+	  shift;;
+    -with-ar|--with-ar) 
+	  ar_spec=yes
+	  ar_exec=$2
+	  shift;;
+    -with-ranlib|--with-ranlib) 
+	  ranlib_spec=yes
+	  ranlib_exec=$2
+	  shift;;
     -byte-only|-byteonly|--byteonly|--byte-only) best_compiler=byte;;
     -debug|--debug) coq_debug_flag=-g;;
     -profile|--profile) coq_profile_flag=-p;;
-     *) echo "Unknown option \"$1\"." 1>&2; exit 2;;
+    *) echo "Unknown option \"$1\"." 1>&2; exit 2;;
   esac
   shift
 done
@@ -619,6 +635,9 @@ sed -e "s|LOCALINSTALLATION|$local|" \
     -e "s|OCAMLLEXEXEC|$ocamllexexec|" \
     -e "s|OCAMLYACCEXEC|$ocamlyaccexec|" \
     -e "s|CAMLMKTOPEXEC|$camlmktopexec|" \
+    -e "s|CCEXEC|$gcc_exec|" \
+    -e "s|AREXEC|$ar_exec|" \
+    -e "s|RANLIBEXEC|$ranlib_exec|" \
     -e "s|STRIPCOMMAND|$STRIPCOMMAND|" \
     -e "s|FSETSOPT|$fsets|" \
     -e "s|REALSOPT|$reals|" \