From 6215d67fd1f94ccd25bb0059e7441ec529fc9ad8 Mon Sep 17 00:00:00 2001
From: Jacques-Pascal Deplaix
Date: Mon, 15 Jan 2018 15:55:18 +0000
Subject: Avoid shell backticks and improve md5sum.ml error messages

---
 Makefile.checker | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'Makefile.checker')

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
 
-- 
cgit v1.2.3