diff options
| author | Maxime Dénès | 2016-07-04 19:48:05 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2016-07-04 19:48:05 +0200 |
| commit | b2f8f9edd5c1bb0a9c8c4f4b049381b979d3e385 (patch) | |
| tree | 32e966816e22fc332007790c48eb810219fe8539 /Makefile.checker | |
| parent | da99355b4d6de31aec5a660f7afe100190a8e683 (diff) | |
| parent | 073178a9821d10b72fe581d3ba7814afd7dfbb05 (diff) | |
Merge remote-tracking branch 'github/pr/229' into trunk
Was PR#229: Bytecode compilation in a new 'make byte' rule apart from 'make world'
Diffstat (limited to 'Makefile.checker')
| -rw-r--r-- | Makefile.checker | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/Makefile.checker b/Makefile.checker index 3ea0baced6..435d8e8f64 100644 --- a/Makefile.checker +++ b/Makefile.checker @@ -71,7 +71,7 @@ checker/%.cmo: checker/%.ml checker/%.cmx: checker/%.ml $(SHOW)'OCAMLOPT $<' - $(HIDE)$(OCAMLOPT) $(CHKLIBS) $(OPTFLAGS) $(HACKMLI) -c $< + $(HIDE)$(OCAMLOPT) $(CHKLIBS) $(OPTFLAGS) -c $< md5chk: $(SHOW)'MD5SUM cic.mli' |