aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorfbesson2009-08-01 10:34:30 +0000
committerfbesson2009-08-01 10:34:30 +0000
commit48465ba75f802c3b05a6621ff4e3de259d2b4008 (patch)
tree50f763293270a5ac65bc1e2f2a398a069c76c474
parente801a25712df6bf28e7dd7dac947d068f4453e5b (diff)
csdpcert + unix
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12256 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r--Makefile.build4
1 files changed, 2 insertions, 2 deletions
diff --git a/Makefile.build b/Makefile.build
index d3abfc8b7e..60156f5098 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -255,12 +255,12 @@ checker/check.cmxa: | checker/check.mllib.d
ifeq ($(BEST),opt)
plugins/micromega/csdpcert$(EXE): $(CSDPCERTCMX)
$(SHOW)'OCAMLOPT -o $@'
- $(HIDE)$(OCAMLOPT) $(OPTFLAGS) nums.cmxa -o $@ $^
+ $(HIDE)$(OCAMLOPT) $(OPTFLAGS) nums.cmxa unix.cmxa -o $@ $^
$(STRIP) $@
else
plugins/micromega/csdpcert$(EXE): $(CSDPCERTCMO)
$(SHOW)'OCAMLC -o $@'
- $(HIDE)$(OCAMLC) $(BYTEFLAGS) nums.cma -o $@ $^
+ $(HIDE)$(OCAMLC) $(BYTEFLAGS) nums.cma unix.cma -o $@ $^
endif
###########################################################################