diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2018-01-18 17:55:54 +0100 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2018-01-18 17:55:54 +0100 |
| commit | f26bf29cfe6fb154400f3a1305b86b34ad88e0e2 (patch) | |
| tree | 2123a95066b6097bfb5105abf46835f31f939780 /Makefile.build | |
| parent | 4d8903c06fd9fd2aca793da8bb55448906347a8c (diff) | |
| parent | 7b9f83224e13b21fcb5bd1b3742f52070c3299e4 (diff) | |
Merge PR #6448: Cleanup and add debug printers a bit
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 d8474ae13..f0dd46b0f 100644 --- a/Makefile.build +++ b/Makefile.build @@ -594,11 +594,14 @@ kernel/kernel.cma: kernel/kernel.mllib $(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) plugins/micromega/%.cmi: plugins/micromega/%.mli $(SHOW)'OCAMLC $<' |