diff options
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 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 |