diff options
| author |  Enrico Tassi <Enrico.Tassi@inria.fr> | 2017-08-29 14:56:31 +0200 |
|---|---|---|
| committer | Enrico Tassi <Enrico.Tassi@inria.fr> | 2017-08-29 17:47:57 +0200 |
| commit | 6e07e3a53e56882043b9db49f03fdf1470a16c46 (patch) | |
| tree | 6170356828a2b762eaba68051a213fc2c791c8d5 /tools | |
| parent | ddced9fa0c3e96925aac9efda39d3fb29e8bdfcd (diff) | |
coq_makefile(pack): ml -> cmx --pack-> cmx -> cmxa -> cmxs
Diffstat (limited to 'tools')
| -rw-r--r-- | tools/CoqMakefile.in | 12 |
1 files changed, 9 insertions, 3 deletions
diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in index fc8c450ec..e919db4a9 100644 --- a/tools/CoqMakefile.in +++ b/tools/CoqMakefile.in @@ -592,9 +592,14 @@ $(MLLIBFILES:.mllib=.cmxa): %.cmxa: | %.mllib $(HIDE)$(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) -a -o $@ $^ -$(MLPACKFILES:.mlpack=.cmxs): %.cmxs: %.cmx +$(MLPACKFILES:.mlpack=.cmxs): %.cmxs: %.cmxa $(SHOW)'CAMLOPT -shared -o $@' - $(HIDE)$(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) -shared -o $@ $< + $(HIDE)$(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) \ + -shared -linkall -o $@ $< + +$(MLPACKFILES:.mlpack=.cmxa): %.cmxa: %.cmx + $(SHOW)'CAMLOPT -a -o $@' + $(HIDE)$(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) -a -o $@ $< $(MLPACKFILES:.mlpack=.cma): %.cma: %.cmo | %.mlpack $(SHOW)'CAMLC -a -o $@' @@ -611,7 +616,8 @@ $(MLPACKFILES:.mlpack=.cmx): %.cmx: | %.mlpack # This rule is for _CoqProject with no .mllib nor .mlpack $(filter-out $(MLLIBFILES:.mllib=.cmxs) $(MLPACKFILES:.mlpack=.cmxs) $(addsuffix .cmxs,$(PACKEDFILES)) $(addsuffix .cmxs,$(LIBEDFILES)),$(MLFILES:.ml=.cmxs) $(ML4FILES:.ml4=.cmxs)): %.cmxs: %.cmx $(SHOW)'[deprecated,use-mllib-or-mlpack] CAMLOPT -shared -o $@' - $(HIDE)$(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) -shared -o $@ $< + $(HIDE)$(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) \ + -shared -o $@ $< ifneq (,$(TIMING)) TIMING_EXTRA = > $<.$(TIMING_EXT) |