aboutsummaryrefslogtreecommitdiffhomepage
path: root/Makefile.build
diff options
context:
space:
mode:
Diffstat (limited to 'Makefile.build')
-rw-r--r--Makefile.build7
1 files changed, 3 insertions, 4 deletions
diff --git a/Makefile.build b/Makefile.build
index 83e3c7ca9..39d177a13 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -406,17 +406,16 @@ $(COQTOPEXE): $(COQTOPBYTE)
cp $< $@
endif
-# Are "-cclib lcoqrun -dllib -lcoqrun" necessary?
+# VMBYTEFLAGS will either contain -custom of the right -dllpath for the VM
$(COQTOPBYTE): $(LINKCMO) $(LIBCOQRUN) $(TOPLOOPCMA) $(COQTOP_BYTE_MLTOP)
$(SHOW)'COQMKTOP -o $@'
$(HIDE)$(OCAMLC) -linkall -linkpkg -I toplevel \
- -I kernel/byterun -dllpath $(abspath kernel/byterun) -cclib -lcoqrun -dllib -lcoqrun \
+ -I kernel/byterun/ -cclib -lcoqrun $(VMBYTEFLAGS) \
$(SYSMOD) -package camlp5.gramlib,compiler-libs.toplevel \
$(LINKCMO) $(BYTEFLAGS) \
$(COQTOP_BYTE_MLTOP) toplevel/coqtop_bin.ml -o $@
-# coqc
-
+# For coqc
COQCCMO:=clib/clib.cma lib/lib.cma toplevel/usage.cmo tools/coqc.cmo
$(COQC): $(call bestobj, $(COQCCMO))