From b2dd4dd979577e4f384750872f7f0e7f9bd8df94 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Tue, 5 Jul 2016 18:22:53 +0200 Subject: Revert "Merge remote-tracking branch 'github/pr/229' into trunk" This reverts commit b2f8f9edd5c1bb0a9c8c4f4b049381b979d3e385, reversing changes made to da99355b4d6de31aec5a660f7afe100190a8e683. Hugo asked for more discussion on this topic, and it was not in the roadmap. I merged it prematurely because I thought there was a consensus. Also, I missed that it was changing coq_makefile. Sorry about that. --- Makefile.checker | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'Makefile.checker') 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' -- cgit v1.2.3