aboutsummaryrefslogtreecommitdiffhomepage
path: root/tools
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2018-01-16 13:39:44 +0100
committerGravatar Maxime Dénès <mail@maximedenes.fr>2018-01-16 13:39:44 +0100
commitf4da0fe96c4784d89e8544e0273e1175f6a4de41 (patch)
tree721b4836c32d5c6b532d936f8a482b52e217ece7 /tools
parentb0ac9d9748440badec581a3a804caec09c6df49d (diff)
parent6215d67fd1f94ccd25bb0059e7441ec529fc9ad8 (diff)
Merge PR #6466: Replace md5sum/md5 calls by an OCaml program
Diffstat (limited to 'tools')
-rw-r--r--tools/md5sum.ml24
1 files changed, 24 insertions, 0 deletions
diff --git a/tools/md5sum.ml b/tools/md5sum.ml
new file mode 100644
index 000000000..2fdcacc83
--- /dev/null
+++ b/tools/md5sum.ml
@@ -0,0 +1,24 @@
+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 ()
+ | exception End_of_file -> close_in ic; Buffer.contents buf
+ in
+ fill ()
+
+let () =
+ match Sys.argv with
+ | [|_; 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>";
+ prerr_endline "Print MD5 (128-bit) checksum of the file content modulo \\r.";
+ exit 1