aboutsummaryrefslogtreecommitdiffhomepage
path: root/configure.ml
diff options
context:
space:
mode:
authorGravatar Jacques-Pascal Deplaix <jp.deplaix@gmail.com>2017-12-21 11:58:14 +0000
committerGravatar Jacques-Pascal Deplaix <jp.deplaix@gmail.com>2017-12-23 18:54:55 +0000
commit569347abdd64ddd20d3fe8b9ac712d566ccf8ea9 (patch)
tree9c3cf031f080a4de81d85394ea45f64f0de9a5c7 /configure.ml
parentdea75d74c222c25f6aa6c38506ac7a51b339e9c6 (diff)
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 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";