diff options
author | Maxime Dénès <mail@maximedenes.fr> | 2018-01-16 13:39:44 +0100 |
---|---|---|
committer | Maxime Dénès <mail@maximedenes.fr> | 2018-01-16 13:39:44 +0100 |
commit | f4da0fe96c4784d89e8544e0273e1175f6a4de41 (patch) | |
tree | 721b4836c32d5c6b532d936f8a482b52e217ece7 /configure.ml | |
parent | b0ac9d9748440badec581a3a804caec09c6df49d (diff) | |
parent | 6215d67fd1f94ccd25bb0059e7441ec529fc9ad8 (diff) |
Merge PR #6466: Replace md5sum/md5 calls by an OCaml program
Diffstat (limited to 'configure.ml')
-rw-r--r-- | configure.ml | 9 |
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"; |