From 6af31414f91065a3a97af32b9151a6010792753a Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Wed, 15 Nov 2017 14:20:00 +0100 Subject: Fix micromega.ml to match generated file and enforce match in make. Mismatch probably caused by c5aca4005. --- Makefile.build | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'Makefile.build') diff --git a/Makefile.build b/Makefile.build index 991942bf0..39b793d2b 100644 --- a/Makefile.build +++ b/Makefile.build @@ -734,8 +734,8 @@ $(MICROMEGAV:.v=.vo) $(MICROMEGAV:.v=.glob) : $(MICROMEGAV) theories/Init/Prelud $(SHOW)'COQC $<' $(HIDE)rm -f $*.glob $(HIDE)$(BOOTCOQC) $< | sed -e '$$d' > $(MICROMEGAGEN) - $(HIDE)cmp -s $(MICROMEGAML) $(MICROMEGAGEN) || \ - echo "Warning: $(MICROMEGAML) and the code generated by $(MICROMEGAV) differ !" + $(HIDE)diff -u --strip-trailing-cr $(MICROMEGAML) $(MICROMEGAGEN) || \ + (2>&1 echo "Error: $(MICROMEGAML) and the code generated by $(MICROMEGAV) differ !" && false) # The general rule for building .vo files : -- cgit v1.2.3