From 569347abdd64ddd20d3fe8b9ac712d566ccf8ea9 Mon Sep 17 00:00:00 2001
From: Jacques-Pascal Deplaix
Date: Thu, 21 Dec 2017 11:58:14 +0000
Subject: Replace md5sum/md5 calls by an OCaml program

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

(limited to 'Makefile.checker')

diff --git a/Makefile.checker b/Makefile.checker
index 7e0f588759..98b4e7d83b 100644
--- a/Makefile.checker
+++ b/Makefile.checker
@@ -77,9 +77,8 @@ checker/%.cmx: checker/%.ml
 
 md5chk:
 	$(SHOW)'MD5SUM cic.mli'
-	$(HIDE)v=`tr -d "\r" < checker/cic.mli | $(MD5SUM) | sed -n -e 's/ .*//' -e '/^/p'`; \
-	       if grep -q "$$v" checker/values.ml; \
-	       then true; else echo "Error: outdated checker/values.ml: $$v" >&2; false; fi
+	$(HIDE)if grep -q `$(OCAML) tools/md5sum.ml checker/cic.mli` checker/values.ml; \
+	       then true; else echo "Error: outdated checker/values.ml"; false; fi
 
 .PHONY: md5chk
 
-- 
cgit v1.2.3


From 47ceedd5a6f726a58ee7b57c4d80ffd2e80549de Mon Sep 17 00:00:00 2001
From: Jacques-Pascal Deplaix
Date: Thu, 21 Dec 2017 12:14:39 +0000
Subject: Check the whole string given by md5sum.ml

---
 Makefile.checker | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'Makefile.checker')

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


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