diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2017-12-18 18:56:37 +0100 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2017-12-18 18:56:37 +0100 |
| commit | fcdddca6124eec4d34e1f57a39aadbd2b082ffcf (patch) | |
| tree | 223cd97353c601729e496fabde16ed06b4cb19de /Makefile.checker | |
| parent | b6e05e2944c2a7976c4ac1f51694b175f52dbaf8 (diff) | |
| parent | ffb7ada29308398746decc538c81b608ca57f88c (diff) | |
Merge PR #6305: Build with windows line endings
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 73d47dfae..7e0f58875 100644 --- a/Makefile.checker +++ b/Makefile.checker @@ -77,8 +77,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 |