From 569347abdd64ddd20d3fe8b9ac712d566ccf8ea9 Mon Sep 17 00:00:00 2001
From: Jacques-Pascal Deplaix <jp.deplaix@gmail.com>
Date: Thu, 21 Dec 2017 11:58:14 +0000
Subject: Replace md5sum/md5 calls by an OCaml program

---
 Makefile.checker |  5 ++---
 configure.ml     |  9 ---------
 tools/md5sum.ml  | 10 ++++++++++
 3 files changed, 12 insertions(+), 12 deletions(-)
 create mode 100644 tools/md5sum.ml

diff --git a/Makefile.checker b/Makefile.checker
index 7e0f58875..98b4e7d83 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 `$(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/configure.ml b/configure.ml
index 06aa5e766..8feec4e1e 100644
--- a/configure.ml
+++ b/configure.ml
@@ -865,13 +865,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, ... *)
 
@@ -1251,8 +1244,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..d6cac9377
--- /dev/null
+++ b/tools/md5sum.ml
@@ -0,0 +1,10 @@
+let () =
+  match Sys.argv with
+  | [|_; file|] ->
+      let md5 = Digest.to_hex (Digest.file file) in
+      print_endline (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.";
+      exit 1
-- 
cgit v1.2.3