diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-10-06 11:45:34 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-10-06 11:45:34 +0000 |
| commit | 3b4b50789e74e7d596199e4b18349a810ae18696 (patch) | |
| tree | d02e021b5f6311a7a8cdfd909ccbac54f4ffa399 /Makefile.build | |
| parent | 37febc09f2f5e8b64fd321bf54e91e6381b4fa33 (diff) | |
Turn mltop.ml4 into a regular ocaml file
The IFDEF's in mltop.ml4 were there to support platforms with
a native ocaml compiler but no dynlink.cmxa, a situation that
should be pretty rare in the Coq community nowadays (playing
with coqtop on ARM, anyone ?). So we now refuse to build
a native coqtop unless dynlink.cmxa exists (cf ./configure),
and we explain how to create a dummy one if necessary
(cf dev/dynlink.ml). This way, we can clean-up mltop.ml,
and remove ugly special rules in Makefile and myocamlbuild
NB: I checked that this shouldn't have any impact on Coq's
debian packages on exotic architectures (arm, mips, ...),
since apparently on these architectures no ocamlopt at all
are shipped, and coq packages are already byte-only
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15879 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'Makefile.build')
| -rw-r--r-- | Makefile.build | 21 |
1 files changed, 0 insertions, 21 deletions
diff --git a/Makefile.build b/Makefile.build index f2fabf918..6efdf95a4 100644 --- a/Makefile.build +++ b/Makefile.build @@ -742,27 +742,6 @@ grammar/grammar.cma: | grammar/grammar.mllib.d $(SHOW)'OCAMLC -a $@' $(HIDE)$(OCAMLC) $(BYTEFLAGS) $^ -linkall -a -o $@ -# toplevel/mltop.ml4 (ifdef Byte) - -## NB: mltop.ml correspond to the byte version (and hence need no special rules) -## while the opt version is in mltop.optml. Since mltop.optml uses mltop.ml.d -## as dependency file, be sure to import the same modules in the different sections -## of the ml4 - -MLTOP:=toplevel/mltop - -$(MLTOP).cmx: $(MLTOP).optml | $(MLTOP).ml.d $(MLTOP).ml4.d - $(SHOW)'OCAMLOPT $<' - $(HIDE)$(OCAMLOPT) $(OPTFLAGS) -c -impl $< -o $@ - -$(MLTOP).ml: $(MLTOP).ml4 config/Makefile # no camlp4deps here - $(SHOW)'CAMLP4O $<' - $(HIDE)$(CAMLP4O) $(PR_O) $(CAMLP4USE) -DByte -DHasDynlink -impl $< -o $@ - -$(MLTOP).optml: $(MLTOP).ml4 config/Makefile # no camlp4deps here - $(SHOW)'CAMLP4O $<' - $(HIDE)$(CAMLP4O) $(PR_O) $(CAMLP4USE) $(NATDYNLINKDEF) -impl $< -o $@ - ide/coqide_main.ml: ide/coqide_main.ml4 $(SHOW)'CAMLP4O $<' $(HIDE)$(CAMLP4O) $(PR_O) $(CAMLP4USE) -impl $< -o $@ |