aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
-rw-r--r--Makefile.build6
-rwxr-xr-xconfigure25
2 files changed, 4 insertions, 27 deletions
diff --git a/Makefile.build b/Makefile.build
index 907ce47c6..14e8487cd 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -174,10 +174,12 @@ CINCLUDES= -I $(CAMLHLIB)
# libcoqrun.a, dllcoqrun.so
+# NB: We used to do a ranlib after ocamlmklib, but it seems that
+# ocamlmklib is already doing it
+
$(LIBCOQRUN): kernel/byterun/coq_jumptbl.h $(BYTERUN)
cd $(dir $(LIBCOQRUN)) && \
$(OCAMLMKLIB) -oc $(COQRUN) $(foreach u,$(BYTERUN),$(notdir $(u)))
- $(RANLIB) $(LIBCOQRUN)
#coq_jumptbl.h is required only if you have GCC 2.0 or later
kernel/byterun/coq_jumptbl.h : kernel/byterun/coq_instruct.h
@@ -957,7 +959,7 @@ checker/%.mllib.d: $(D_DEPEND_BEFORE_SRC) checker/%.mllib $(D_DEPEND_AFTER_SRC)
%.c.d: $(D_DEPEND_BEFORE_SRC) %.c $(D_DEPEND_AFTER_SRC) $(GENHFILES)
$(SHOW)'CCDEP $<'
- $(HIDE)$(CC) -MM -MQ "$@" -MQ "$(<:.c=.o)" $(CFLAGS) -isystem $(CAMLHLIB) $< $(TOTARGET)
+ $(HIDE)$(OCAMLC) -ccopt "-MM -MQ $@ -MQ $(<:.c=.o) -isystem $(CAMLHLIB)" $< $(TOTARGET)
###########################################################################
# this sets up developper supporting stuff
diff --git a/configure b/configure
index 3db167273..532d0f9bf 100755
--- a/configure
+++ b/configure
@@ -81,10 +81,6 @@ usage () {
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 "-with-cc <file>"
- echo "-with-ar <file>"
- echo "-with-ranlib <file>"
- printf "\tTells configure where to find gcc/ar/ranlib executables\n"
echo "-byte-only"
printf "\tCompiles only bytecode version of Coq\n"
echo "-debug"
@@ -123,10 +119,6 @@ best_compiler=opt
cflags="-fno-defer-pop -Wall -Wno-unused"
natdynlink=yes
-gcc_exec=gcc
-ar_exec=ar
-ranlib_exec=ranlib
-
local=false
coqrunbyteflags_spec=no
coqtoolsbyteflags_spec=no
@@ -258,18 +250,6 @@ 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;;
-makecmd|--makecmd) makecmd="$2"
shift;;
-byte-only|-byteonly|--byteonly|--byte-only) best_compiler=byte;;
@@ -1238,11 +1218,6 @@ BEST=$best_compiler
ARCH=$ARCH
HASNATDYNLINK=$NATDYNLINKFLAG
-# Your C compiler and co
-CC="$gcc_exec"
-AR="$ar_exec"
-RANLIB="$ranlib_exec"
-
# Supplementary libs for some systems, currently:
# . Sun Solaris: -cclib -lunix -cclib -lnsl -cclib -lsocket
# . others : -cclib -lunix