diff options
| -rw-r--r-- | Makefile.checker | 5 | ||||
| -rw-r--r-- | configure.ml | 9 | ||||
| -rw-r--r-- | tools/md5sum.ml | 24 |
3 files changed, 26 insertions, 12 deletions
diff --git a/Makefile.checker b/Makefile.checker index 8334b6a2a..0e429fe86 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 "^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 diff --git a/configure.ml b/configure.ml index e991eadac..ff767d96b 100644 --- a/configure.ml +++ b/configure.ml @@ -861,13 +861,6 @@ let strip = if strip = "" then "strip" else strip end -(** * md5sum command *) - -let md5sum = - select_command "Don’t know how to compute MD5 checksums…" [ - "md5sum", [], [ "--version" ]; - "md5", ["-q"], [ "-s" ; "''" ]; - ] (** * Documentation : do we have latex, hevea, ... *) @@ -1246,8 +1239,6 @@ let write_makefile f = pr "# Unix systems and profiling: true\n"; pr "# Unix systems and no profiling: strip\n"; pr "STRIP=%s\n\n" strip; - pr "#the command md5sum\n"; - pr "MD5SUM=%s\n\n" md5sum; pr "# LablGTK\n"; pr "COQIDEINCLUDES=%s\n\n" !lablgtkincludes; pr "# CoqIde (no/byte/opt)\n"; 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 |