aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar Jacques-Pascal Deplaix <jp.deplaix@gmail.com>2018-01-15 15:55:18 +0000
committerGravatar Jacques-Pascal Deplaix <jp.deplaix@gmail.com>2018-01-15 16:22:19 +0000
commit6215d67fd1f94ccd25bb0059e7441ec529fc9ad8 (patch)
tree67b61720949b49dd9c0063821dc22b5f5fe7be3b
parent47ceedd5a6f726a58ee7b57c4d80ffd2e80549de (diff)
Avoid shell backticks and improve md5sum.ml error messages
-rw-r--r--Makefile.checker4
-rw-r--r--tools/md5sum.ml7
2 files changed, 6 insertions, 5 deletions
diff --git a/Makefile.checker b/Makefile.checker
index e9881d025..4e20631a6 100644
--- a/Makefile.checker
+++ b/Makefile.checker
@@ -77,8 +77,8 @@ checker/%.cmx: checker/%.ml
md5chk:
$(SHOW)'MD5SUM cic.mli'
- $(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
+ $(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/tools/md5sum.ml b/tools/md5sum.ml
index 16bbdb579..2fdcacc83 100644
--- a/tools/md5sum.ml
+++ b/tools/md5sum.ml
@@ -7,8 +7,9 @@ let get_content file =
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
- try fill () with End_of_file -> Buffer.contents buf
+ fill ()
let () =
match Sys.argv with
@@ -18,6 +19,6 @@ let () =
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.";
+ prerr_endline "Usage: ocaml md5sum.ml <FILE>";
+ prerr_endline "Print MD5 (128-bit) checksum of the file content modulo \\r.";
exit 1