diff options
| author | Emilio Jesus Gallego Arias | 2018-11-09 19:15:54 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2018-11-09 19:15:54 +0100 |
| commit | ce8e37b97ce9db6f39368c50fb0ee4a7839ce754 (patch) | |
| tree | a6678760bcd97cf004ba1f065352c8cad666bec3 /Makefile.checker | |
| parent | 7e3c54c09bdd748e2e2a60a94891b65481776041 (diff) | |
| parent | a7522a0ea76a6efaed9342d08a95363b56d88d32 (diff) | |
Merge PR #8949: Remove checker printers
Diffstat (limited to 'Makefile.checker')
| -rw-r--r-- | Makefile.checker | 11 |
1 files changed, 1 insertions, 10 deletions
diff --git a/Makefile.checker b/Makefile.checker index a0f0778d49..7440c767e6 100644 --- a/Makefile.checker +++ b/Makefile.checker @@ -59,8 +59,7 @@ checker/check.cmxa: checker/check.mllib $(SHOW)'OCAMLOPT -a -o $@' $(HIDE)$(OCAMLOPT) $(CHKLIBS) $(OPTFLAGS) -a -o $@ $(filter-out %.mllib, $^) -CHECKMLFILES:=$(filter checker/%, $(MLFILES) $(MLIFILES)) \ - $(filter dev/checker_%, $(MLFILES) $(MLIFILES)) +CHECKMLFILES:=$(filter checker/%, $(MLFILES) $(MLIFILES)) $(CHECKMLDFILE).d: $(filter checker/%, $(MLFILES) $(MLIFILES)) $(SHOW)'OCAMLDEP checker/MLFILES checker/MLIFILES' @@ -82,14 +81,6 @@ checker/%.cmx: checker/%.ml $(SHOW)'OCAMLOPT $<' $(HIDE)$(OCAMLOPT) $(CHKLIBS) $(OPTFLAGS) -c $< -dev/checker_%.cmo: dev/checker_%.ml - $(SHOW)'OCAMLC $<' - $(HIDE)$(OCAMLC) $(CHKLIBS) $(BYTEFLAGS) -I dev/ -c $< - -dev/checker_%.cmi: dev/checker_%.mli - $(SHOW)'OCAMLC $<' - $(HIDE)$(OCAMLC) $(CHKLIBS) $(BYTEFLAGS) -I dev/ -c $< - # For emacs: # Local Variables: # mode: makefile |