diff options
| author | Maxime Dénès | 2017-11-20 10:38:47 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2017-11-20 10:38:47 +0100 |
| commit | 07c5e013cbe9aac299881bdde3e1d44af0d35fa8 (patch) | |
| tree | 3d28c4bed80fc7d8ecc25b9d32d112f9b5cbce81 /Makefile.build | |
| parent | 9d3a07d9a7ddf3a0e33b6b1f60d3c89037dc55b7 (diff) | |
| parent | 6af31414f91065a3a97af32b9151a6010792753a (diff) | |
Merge PR #6161: Fix micromega.ml to match generated file and enforce match in make.
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 991942bf0a..39b793d2bb 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 : |