From 47ceedd5a6f726a58ee7b57c4d80ffd2e80549de Mon Sep 17 00:00:00 2001 From: Jacques-Pascal Deplaix Date: Thu, 21 Dec 2017 12:14:39 +0000 Subject: Check the whole string given by md5sum.ml --- Makefile.checker | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'Makefile.checker') diff --git a/Makefile.checker b/Makefile.checker index 98b4e7d83..e9881d025 100644 --- a/Makefile.checker +++ b/Makefile.checker @@ -77,7 +77,7 @@ checker/%.cmx: checker/%.ml md5chk: $(SHOW)'MD5SUM cic.mli' - $(HIDE)if grep -q `$(OCAML) tools/md5sum.ml checker/cic.mli` checker/values.ml; \ + $(HIDE)if grep -q "^MD5 `$(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