aboutsummaryrefslogtreecommitdiffhomepage
path: root/dev
diff options
context:
space:
mode:
authorGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2009-03-31 17:08:27 +0000
committerGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2009-03-31 17:08:27 +0000
commitcd048fabb1cca67c782d41f6ce294a92fbb42ee2 (patch)
treee0e4c3648c7913d8e4b7a98e516ce6ed9ce5da79 /dev
parent99c8916342ce6b13661aa1076b4e8444c6e97cb6 (diff)
Complementary fix to have ocamlopt_shared_os5fix.sh working correctly
(tested on MacOS 10.5). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12042 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'dev')
-rwxr-xr-xdev/ocamlopt_shared_os5fix.sh6
1 files changed, 3 insertions, 3 deletions
diff --git a/dev/ocamlopt_shared_os5fix.sh b/dev/ocamlopt_shared_os5fix.sh
index 6782d2fa0..f7d31ad81 100755
--- a/dev/ocamlopt_shared_os5fix.sh
+++ b/dev/ocamlopt_shared_os5fix.sh
@@ -10,9 +10,9 @@ BASE=`basename $CMXS .cmxs`
CMXA=$DIR/$BASE.cmxa
ARC=$DIR/$BASE.a
# we assume that all object files are at the same place than the rest
-OBJS=`ar t $ARC | sed -e "s|^|$DIR/|"`
+OBJS=`ar t $ARC | sed -e "s|^|$DIR/|" | grep -v SYMDEF`
-"$OCAMLOPT" -dstartup -linkall -shared -o $CMXS $CMXA
+$OCAMLOPT -dstartup -linkall -shared -o $CMXS $CMXA
# Fix1: add a dummy instruction before the caml generic functions
# Fix2: make all caml generic functions private
rm -f $CMXS $CMXS.startup.fixed.s
@@ -25,5 +25,5 @@ cat $CMXS.startup.s | sed \
# Recompile fixed startup code
as -o $CMXS.startup.o $CMXS.startup.fixed.s
# Build fixed .cmxs (assume all object files are at the same place)
-ld -bundle -flat_namespace -undefined warning -read_only_relocs suppress -o $CMXS $OBJS
+ld -bundle -flat_namespace -undefined warning -read_only_relocs suppress -o $CMXS $OBJS $CMXS.startup.o
rm $CMXS.startup.o $CMXS.startup.s $CMXS.startup.fixed.s \ No newline at end of file