diff options
| author |  Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2017-12-16 10:58:52 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2017-12-22 16:36:32 +0100 |
| commit | 87cbd64254f33439882156d9a297a6a2f6886057 (patch) | |
| tree | 8ffc7a81a0018c0a7d91c24871c84da00bea4996 /Makefile.build | |
| parent | 50bd89748af03bb28ad7024f2ceef500489a91b0 (diff) | |
Cleanup debug printers a bit, add generated mli.
Diffstat (limited to 'Makefile.build')
| -rw-r--r-- | Makefile.build | 7 |
1 files changed, 5 insertions, 2 deletions
diff --git a/Makefile.build b/Makefile.build index 940943c41..a9dbc4b44 100644 --- a/Makefile.build +++ b/Makefile.build @@ -595,11 +595,14 @@ API/API.cmi : API/API.mli $(SHOW)'OCAMLOPT -pack -o $@' $(HIDE)$(OCAMLOPT) $(MLINCLUDES) $(OPTFLAGS) -pack -o $@ $(filter-out %.mlpack, $^) +COND_IDEFLAGS=$(if $(filter tools/fake_ide% tools/coq_makefile%,$<), -I ide,) +COND_PRINTERFLAGS=$(if $(filter dev/%,$<), -I dev,) + COND_BYTEFLAGS= \ - $(if $(filter tools/fake_ide% tools/coq_makefile%,$<), -I ide,) $(MLINCLUDES) $(BYTEFLAGS) + $(COND_IDEFLAGS) $(COND_PRINTERFLAGS) $(MLINCLUDES) $(BYTEFLAGS) COND_OPTFLAGS= \ - $(if $(filter tools/fake_ide% tools/coq_makefile%,$<), -I ide,) $(MLINCLUDES) $(OPTFLAGS) + $(COND_IDEFLAGS) $(MLINCLUDES) $(OPTFLAGS) %.cmi: %.mli $(SHOW)'OCAMLC $<' |