aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar glondu <glondu@85f007b7-540e-0410-9357-904b9bb8a0f7>2008-09-05 06:08:45 +0000
committerGravatar glondu <glondu@85f007b7-540e-0410-9357-904b9bb8a0f7>2008-09-05 06:08:45 +0000
commit0f4d785afdcca74dd84f75d3b487a64e624fb66c (patch)
treeb3867e7e16b5fe75a5413a4e3479352b68645d0b
parentc28fdc2abf986c960da646e11556cefaa7d101e4 (diff)
Build coqrun library using ocamlmklib...
...instead of plain ar, so that .so (and .dll) is also created. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11362 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r--Makefile.build5
-rw-r--r--Makefile.common4
-rw-r--r--config/Makefile.template1
-rwxr-xr-xconfigure2
4 files changed, 9 insertions, 3 deletions
diff --git a/Makefile.build b/Makefile.build
index 658abcf5c..0a60e4bb8 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -137,10 +137,11 @@ endif
CINCLUDES= -I $(CAMLHLIB)
-# libcoqrun.a
+# libcoqrun.a, dllcoqrun.so
$(LIBCOQRUN): kernel/byterun/coq_jumptbl.h $(BYTERUN)
- $(AR) rc $(LIBCOQRUN) $(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
diff --git a/Makefile.common b/Makefile.common
index 08ae6f835..5c8c28cd3 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -111,7 +111,9 @@ REFMANPNGFILES:=$(REFMANEPSFILES:.eps=.png)
# Object and Source files
###########################################################################
-LIBCOQRUN:=kernel/byterun/libcoqrun.a
+COQRUN := coqrun
+LIBCOQRUN:=kernel/byterun/lib$(COQRUN).a
+DLLCOQRUN:=$(dir $(LIBCOQRUN))dll$(COQRUN).so
CLIBS:=unix.cma
diff --git a/config/Makefile.template b/config/Makefile.template
index fc8af173f..a48bbceb9 100644
--- a/config/Makefile.template
+++ b/config/Makefile.template
@@ -58,6 +58,7 @@ COQIDEINCLUDES=LABLGTKINCLUDES
# Objective-Caml compile command
OCAML="OCAMLEXEC"
OCAMLC="BYTECAMLC"
+OCAMLMKLIB="OCAMLMKLIBEXEC"
OCAMLOPT="NATIVECAMLC"
OCAMLDEP="OCAMLDEPEXEC"
OCAMLDOC="OCAMLDOCEXEC"
diff --git a/configure b/configure
index 6681c91b5..dc1baaffa 100755
--- a/configure
+++ b/configure
@@ -83,6 +83,7 @@ usage () {
# Default OCaml binaries
bytecamlc=ocamlc
nativecamlc=ocamlopt
+ocamlmklib=ocamlmklib
ocamlexec=ocaml
ocamldepexec=ocamldep
ocamldocexec=ocamldoc
@@ -937,6 +938,7 @@ sed -e "s|LOCALINSTALLATION|$local|" \
-e "s|BESTCOMPILER|$best_compiler|" \
-e "s|EXECUTEEXTENSION|$EXE|" \
-e "s|BYTECAMLC|$bytecamlc|" \
+ -e "s|OCAMLMKLIBEXEC|$ocamlmklib|" \
-e "s|NATIVECAMLC|$nativecamlc|" \
-e "s|OCAMLEXEC|$ocamlexec|" \
-e "s|OCAMLDEPEXEC|$ocamldepexec|" \