From cd048fabb1cca67c782d41f6ce294a92fbb42ee2 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 31 Mar 2009 17:08:27 +0000
Subject: 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
---
 Makefile.build | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'Makefile.build')

diff --git a/Makefile.build b/Makefile.build
index d8531e88f6..e7e409833a 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -837,7 +837,7 @@ endif
 %.cmxs: %.cmxa
 	$(SHOW)'OCAMLOPT -shared -o $@'
 ifeq ($(HASNATDYNLINK),os5fixme)
-	$(HIDE)dev/ocamlopt_shared_os5fix.sh '$(OCAMLOPT)' $@
+	$(HIDE)dev/ocamlopt_shared_os5fix.sh "$(OCAMLOPT)" $@
 else
 	$(HIDE)$(OCAMLOPT) -linkall -shared -o $@ $<
 endif
-- 
cgit v1.2.3