aboutsummaryrefslogtreecommitdiffhomepage
path: root/Makefile.checker
diff options
context:
space:
mode:
Diffstat (limited to 'Makefile.checker')
-rw-r--r--Makefile.checker2
1 files changed, 1 insertions, 1 deletions
diff --git a/Makefile.checker b/Makefile.checker
index 3ea0baced..435d8e8f6 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'