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";