diff options
Diffstat (limited to 'Makefile.checker')
| -rw-r--r-- | Makefile.checker | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/Makefile.checker b/Makefile.checker index e9881d025..4e20631a6 100644 --- a/Makefile.checker +++ b/Makefile.checker @@ -77,8 +77,8 @@ checker/%.cmx: checker/%.ml md5chk: $(SHOW)'MD5SUM cic.mli' - $(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 + $(HIDE)if grep -q "^MD5 $$($(OCAML) tools/md5sum.ml checker/cic.mli)$$" checker/values.ml; \ + then true; else echo "Error: outdated checker/values.ml" >&2; false; fi .PHONY: md5chk |