diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2018-01-16 13:39:44 +0100 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2018-01-16 13:39:44 +0100 |
| commit | f4da0fe96c4784d89e8544e0273e1175f6a4de41 (patch) | |
| tree | 721b4836c32d5c6b532d936f8a482b52e217ece7 /Makefile.checker | |
| parent | b0ac9d9748440badec581a3a804caec09c6df49d (diff) | |
| parent | 6215d67fd1f94ccd25bb0059e7441ec529fc9ad8 (diff) | |
Merge PR #6466: Replace md5sum/md5 calls by an OCaml program
Diffstat (limited to 'Makefile.checker')
| -rw-r--r-- | Makefile.checker | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/Makefile.checker b/Makefile.checker index 8334b6a2a..0e429fe86 100644 --- a/Makefile.checker +++ b/Makefile.checker @@ -77,9 +77,8 @@ checker/%.cmx: checker/%.ml md5chk: $(SHOW)'MD5SUM cic.mli' - $(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 + $(HIDE)if grep -q "^MD5 $$($(OCAML) tools/md5sum.ml checker/cic.mli)$$" checker/values.ml; \ + then true; else echo "Error: outdated checker/values.ml" >&2; false; fi .PHONY: md5chk |