diff options
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 435d8e8f6..3ea0baced 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) -c $< + $(HIDE)$(OCAMLOPT) $(CHKLIBS) $(OPTFLAGS) $(HACKMLI) -c $< md5chk: $(SHOW)'MD5SUM cic.mli' |