aboutsummaryrefslogtreecommitdiffhomepage
path: root/tools
diff options
context:
space:
mode:
authorGravatar Jacques-Pascal Deplaix <jp.deplaix@gmail.com>2017-12-21 12:14:39 +0000
committerGravatar Jacques-Pascal Deplaix <jp.deplaix@gmail.com>2017-12-24 13:42:03 +0000
commit47ceedd5a6f726a58ee7b57c4d80ffd2e80549de (patch)
tree4b05ddcf8bbb5bc99b762416c4d2605df10d5e83 /tools
parent569347abdd64ddd20d3fe8b9ac712d566ccf8ea9 (diff)
Check the whole string given by md5sum.ml
Diffstat (limited to 'tools')
-rw-r--r--tools/md5sum.ml17
1 files changed, 15 insertions, 2 deletions
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]";