aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-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
###########################################################################