aboutsummaryrefslogtreecommitdiffhomepage
path: root/Makefile.build
diff options
context:
space:
mode:
Diffstat (limited to 'Makefile.build')
-rw-r--r--Makefile.build24
1 files changed, 24 insertions, 0 deletions
diff --git a/Makefile.build b/Makefile.build
index 33ab72e68..5c454a145 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -606,10 +606,26 @@ COND_BYTEFLAGS= \
COND_OPTFLAGS= \
$(if $(filter tools/fake_ide% tools/coq_makefile%,$<), -I ide,) $(MLINCLUDES) $(OPTFLAGS)
+plugins/micromega/%.cmi: plugins/micromega/%.mli
+ $(SHOW)'OCAMLC $<'
+ $(HIDE)$(OCAMLC) $(COND_BYTEFLAGS) -package unix,num -c $<
+
+plugins/nsatz/%.cmi: plugins/nsatz/%.mli
+ $(SHOW)'OCAMLC $<'
+ $(HIDE)$(OCAMLC) $(COND_BYTEFLAGS) -package unix,num -c $<
+
%.cmi: %.mli
$(SHOW)'OCAMLC $<'
$(HIDE)$(OCAMLC) $(COND_BYTEFLAGS) -c $<
+plugins/micromega/%.cmo: plugins/micromega/%.ml
+ $(SHOW)'OCAMLC $<'
+ $(HIDE)$(OCAMLC) $(COND_BYTEFLAGS) -package unix,num -c $<
+
+plugins/nsatz/%.cmo: plugins/nsatz/%.ml
+ $(SHOW)'OCAMLC $<'
+ $(HIDE)$(OCAMLC) $(COND_BYTEFLAGS) -package unix,num -c $<
+
%.cmo: %.ml
$(SHOW)'OCAMLC $<'
$(HIDE)$(OCAMLC) $(COND_BYTEFLAGS) -c $<
@@ -643,6 +659,14 @@ plugins/micromega/sos_FORPACK:=
plugins/micromega/sos_print_FORPACK:=
plugins/micromega/csdpcert_FORPACK:=
+plugins/micromega/%.cmx: plugins/micromega/%.ml
+ $(SHOW)'OCAMLOPT $<'
+ $(HIDE)$(OCAMLOPT) $(COND_OPTFLAGS) $(HACKMLI) $($(@:.cmx=_FORPACK)) -package unix,num -c $<
+
+plugins/nsatz/%.cmx: plugins/nsatz/%.ml
+ $(SHOW)'OCAMLOPT $<'
+ $(HIDE)$(OCAMLOPT) $(COND_OPTFLAGS) $(HACKMLI) $($(@:.cmx=_FORPACK)) -package unix,num -c $<
+
plugins/%.cmx: plugins/%.ml
$(SHOW)'OCAMLOPT $<'
$(HIDE)$(OCAMLOPT) $(COND_OPTFLAGS) $(HACKMLI) $($(@:.cmx=_FORPACK)) -c $<