aboutsummaryrefslogtreecommitdiffhomepage
path: root/configure.ml
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 /configure.ml
parentb0ac9d9748440badec581a3a804caec09c6df49d (diff)
parent6215d67fd1f94ccd25bb0059e7441ec529fc9ad8 (diff)
Merge PR #6466: Replace md5sum/md5 calls by an OCaml program
Diffstat (limited to 'configure.ml')
-rw-r--r--configure.ml9
1 files changed, 0 insertions, 9 deletions
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";