diff options
author | Jacques-Pascal Deplaix <jp.deplaix@gmail.com> | 2017-12-21 12:14:39 +0000 |
---|---|---|
committer | Jacques-Pascal Deplaix <jp.deplaix@gmail.com> | 2017-12-24 13:42:03 +0000 |
commit | 47ceedd5a6f726a58ee7b57c4d80ffd2e80549de (patch) | |
tree | 4b05ddcf8bbb5bc99b762416c4d2605df10d5e83 | |
parent | 569347abdd64ddd20d3fe8b9ac712d566ccf8ea9 (diff) |
Check the whole string given by md5sum.ml
-rw-r--r-- | Makefile.checker | 2 | ||||
-rw-r--r-- | 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]"; |