diff options
| author | Maxime Dénès | 2017-05-28 18:12:46 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-05-28 18:12:46 +0200 |
| commit | 422b892e71641f23dc71499733997546ecffa46b (patch) | |
| tree | 64931e62dece87071d9bac59e306707bf8669934 /tools | |
| parent | 7816815c01c6338dbd3447bad6ff2fcca415e139 (diff) | |
| parent | 7d5873c1008a458247517d0c6200c0004340fd63 (diff) | |
Merge PR#683: coq_makefile: build .cma for each .mlpack
Diffstat (limited to 'tools')
| -rw-r--r-- | tools/CoqMakefile.in | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in index 5231899c6e..fb064c495f 100644 --- a/tools/CoqMakefile.in +++ b/tools/CoqMakefile.in @@ -184,7 +184,7 @@ CMOFILES = \ $(MLPACKFILES:.mlpack=.cmo) CMXFILES = $(CMOFILES:.cmo=.cmx) OFILES = $(CMXFILES:.cmx=.o) -CMAFILES = $(MLLIBFILES:.mllib=.cma) +CMAFILES = $(MLLIBFILES:.mllib=.cma) $(MLPACKFILES:.mlpack=.cma) CMXAFILES = $(CMAFILES:.cma=.cmxa) CMIFILES = \ $(CMOFILES:.cmo=.cmi) \ @@ -474,6 +474,10 @@ $(MLPACKFILES:.mlpack=.cmxs): %.cmxs: %.cmx $(SHOW)'CAMLOPT -shared -o $@' $(HIDE)$(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) -shared -o $@ $< +$(MLPACKFILES:.mlpack=.cma): %.cma: %.cmo | %.mlpack + $(SHOW)'CAMLC -a -o $@' + $(HIDE)$(CAMLLINK) $(CAMLDEBUG) $(CAMLFLAGS) -a -o $@ $^ + $(MLPACKFILES:.mlpack=.cmo): %.cmo: | %.mlpack $(SHOW)'CAMLC -pack -o $@' $(HIDE)$(CAMLLINK) $(CAMLDEBUG) $(CAMLFLAGS) -pack -o $@ $^ |