diff options
| author | Jim | 2017-12-01 10:24:57 -0800 |
|---|---|---|
| committer | Jim Fehrle | 2017-12-16 10:38:30 -0800 |
| commit | 84cdfdf1871997931a866949b6c14198e01a3136 (patch) | |
| tree | 1ee62ae0e511ffadd5918fde50745b8fe435b433 /Makefile.checker | |
| parent | 0275b5802ffd416dd0ed739955445a1c3c0287e9 (diff) | |
For bug 6249, Segmentation fault when building Coq on Windows 10.
Enable builds on Windows by removing Windows-style endings where it impacts make.
The fix in Makefile.build is a band-aid fix; maximedenes said he would remove the dependency on sed and awk here.
Diffstat (limited to 'Makefile.checker')
| -rw-r--r-- | Makefile.checker | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/Makefile.checker b/Makefile.checker index 435d8e8f64..f9ed2d9571 100644 --- a/Makefile.checker +++ b/Makefile.checker @@ -75,8 +75,9 @@ checker/%.cmx: checker/%.ml md5chk: $(SHOW)'MD5SUM cic.mli' - $(HIDE)if grep -q `$(MD5SUM) checker/cic.mli` checker/values.ml; \ - then true; else echo "Error: outdated checker/values.ml"; false; fi + $(HIDE)v=`tr -d "\r" < checker/cic.mli | $(MD5SUM) | sed -n -e 's/ .*//' -e '/^/p'`; \ + if grep -q "$$v" checker/values.ml; \ + then true; else echo "Error: outdated checker/values.ml: $$v" >&2; false; fi .PHONY: md5chk |