From 569347abdd64ddd20d3fe8b9ac712d566ccf8ea9 Mon Sep 17 00:00:00 2001 From: Jacques-Pascal Deplaix Date: Thu, 21 Dec 2017 11:58:14 +0000 Subject: Replace md5sum/md5 calls by an OCaml program --- Makefile.checker | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) (limited to 'Makefile.checker') diff --git a/Makefile.checker b/Makefile.checker index 7e0f588759..98b4e7d83b 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 -- cgit v1.2.3