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

---
 Makefile.checker |  2 +-
 tools/md5sum.ml  | 17 +++++++++++++++--
 2 files changed, 16 insertions(+), 3 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
diff --git a/tools/md5sum.ml b/tools/md5sum.ml
index d6cac9377..16bbdb579 100644
--- a/tools/md5sum.ml
+++ b/tools/md5sum.ml
@@ -1,8 +1,21 @@
+let get_content file =
+  let ic = open_in_bin file in
+  let buf = Buffer.create 2048 in
+  let rec fill () =
+    match input_char ic with
+    | '\r' -> fill () (* NOTE: handles the case on Windows where the
+                         git checkout has included return characters.
+                         See: https://github.com/coq/coq/pull/6305 *)
+    | c -> Buffer.add_char buf c; fill ()
+  in
+  try fill () with End_of_file -> Buffer.contents buf
+
 let () =
   match Sys.argv with
   | [|_; file|] ->
-      let md5 = Digest.to_hex (Digest.file file) in
-      print_endline (md5 ^ "  " ^ file)
+      let content = get_content file in
+      let md5 = Digest.to_hex (Digest.string content) in
+      print_string (md5 ^ " " ^ file)
   | _ ->
       prerr_endline "Error: This program needs exactly one parameter.";
       prerr_endline "Usage: ocaml md5sum.ml [FILE]";
-- 
cgit v1.2.3