diff options
| author |  Jacques-Pascal Deplaix <jp.deplaix@gmail.com> | 2017-12-21 11:58:14 +0000 |
|---|---|---|
| committer | Jacques-Pascal Deplaix <jp.deplaix@gmail.com> | 2017-12-23 18:54:55 +0000 |
| commit | 569347abdd64ddd20d3fe8b9ac712d566ccf8ea9 (patch) | |
| tree | 9c3cf031f080a4de81d85394ea45f64f0de9a5c7 /Makefile.checker | |
| parent | dea75d74c222c25f6aa6c38506ac7a51b339e9c6 (diff) | |
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 7e0f58875..98b4e7d83 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 `$(OCAML) tools/md5sum.ml checker/cic.mli` checker/values.ml; \ + then true; else echo "Error: outdated checker/values.ml"; false; fi .PHONY: md5chk |