diff options
| author | Jacques-Pascal Deplaix | 2017-12-21 12:14:39 +0000 |
|---|---|---|
| committer | Jacques-Pascal Deplaix | 2017-12-24 13:42:03 +0000 |
| commit | 47ceedd5a6f726a58ee7b57c4d80ffd2e80549de (patch) | |
| tree | 4b05ddcf8bbb5bc99b762416c4d2605df10d5e83 /Makefile.checker | |
| parent | 569347abdd64ddd20d3fe8b9ac712d566ccf8ea9 (diff) | |
Check the whole string given by md5sum.ml
Diffstat (limited to 'Makefile.checker')
| -rw-r--r-- | Makefile.checker | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/Makefile.checker b/Makefile.checker index 98b4e7d83b..e9881d025e 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 |