diff options
| author | Jacques-Pascal Deplaix | 2018-01-15 15:55:18 +0000 |
|---|---|---|
| committer | Jacques-Pascal Deplaix | 2018-01-15 16:22:19 +0000 |
| commit | 6215d67fd1f94ccd25bb0059e7441ec529fc9ad8 (patch) | |
| tree | 67b61720949b49dd9c0063821dc22b5f5fe7be3b /Makefile.checker | |
| parent | 47ceedd5a6f726a58ee7b57c4d80ffd2e80549de (diff) | |
Avoid shell backticks and improve md5sum.ml error messages
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 e9881d025e..4e20631a6e 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 |