diff options
| author |  Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2017-11-15 14:20:00 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2017-11-16 14:23:07 +0100 |
| commit | 6af31414f91065a3a97af32b9151a6010792753a (patch) | |
| tree | 29242ed58354aa4290e050df073c926b754a498d /Makefile.build | |
| parent | a2b02cb9142984b912bf01cea09449d767326f19 (diff) | |
Fix micromega.ml to match generated file and enforce match in make.
Mismatch probably caused by c5aca4005.
Diffstat (limited to 'Makefile.build')
| -rw-r--r-- | Makefile.build | 4 |
1 files changed, 2 insertions, 2 deletions
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 : |