aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
-rw-r--r--Makefile.build1
-rw-r--r--config/Makefile.template1
-rwxr-xr-xconfigure7
3 files changed, 7 insertions, 2 deletions
diff --git a/Makefile.build b/Makefile.build
index f6568e5b0..99dfdd23a 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -669,6 +669,7 @@ endif
# we install it with libraries
-$(MKDIR) -p $(FULLCOQLIB)/contrib/micromega
$(INSTALLBIN) $(CSDPCERT) $(FULLCOQLIB)/contrib/micromega
+ $(INSTALLBIN) $(DLLCOQRUN) $(FULLCOQLIB)
install-library-light:
$(MKDIR) $(FULLCOQLIB)
diff --git a/config/Makefile.template b/config/Makefile.template
index e617d3793..e0e7bf0b0 100644
--- a/config/Makefile.template
+++ b/config/Makefile.template
@@ -23,6 +23,7 @@ LOCAL=LOCALINSTALLATION
# Bytecode link flags for VM ("-custom" or "-dllib -lcoqrun")
COQRUNBYTEFLAGS=XCOQRUNBYTEFLAGS
+BUILDLDPATH=
# Paths for true installation
# BINDIR=path where coqtop, coqc, coqmktop, coq-tex, coqdep, gallina and
diff --git a/configure b/configure
index e4148c7a4..b9f44b9b6 100755
--- a/configure
+++ b/configure
@@ -764,10 +764,12 @@ case $coqdocdir_spec/$prefix_spec/$local in
esac;;
esac
+BUILDLDPATH="# you might want to set CAML_LD_LIBRARY_PATH by hand!"
case $coqrunbyteflags_spec/$local in
yes/*) COQRUNBYTEFLAGS="$coqrunbyteflags";;
- */true) COQRUNBYTEFLAGS="-custom";;
- *) COQRUNBYTEFLAGS="-custom";;
+ */true) COQRUNBYTEFLAGS="-dllib -lcoqrun -dllpath $COQTOP/kernel/byterun";;
+ *) COQRUNBYTEFLAGS="-dllib -lcoqrun -dllpath $LIBDIR"
+ BUILDLDPATH="export CAML_LD_LIBRARY_PATH=$COQTOP/kernel/byterun";;
esac
# case $emacs_spec in
@@ -932,6 +934,7 @@ sed -e "s|LOCALINSTALLATION|$local|" \
-e "s|COQVERSION|$VERSION|" \
-e "s|BINDIRDIRECTORY|$ESCBINDIR|" \
-e "s|COQLIBDIRECTORY|$ESCLIBDIR|" \
+ -e "s|BUILDLDPATH=|$BUILDLDPATH|" \
-e "s|MANDIRDIRECTORY|$ESCMANDIR|" \
-e "s|DOCDIRDIRECTORY|$ESCDOCDIR|" \
-e "s|EMACSLIBDIRECTORY|$ESCEMACSLIB|" \