From 369a0c9354497639d96ba2fef94c920e051d00fb Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Mon, 17 Aug 2015 16:02:35 +0200
Subject: Remove duplicate code.

---
 configure.ml | 6 ------
 1 file changed, 6 deletions(-)

diff --git a/configure.ml b/configure.ml
index d509aa70e0..3fe34d6cae 100644
--- a/configure.ml
+++ b/configure.ml
@@ -838,12 +838,6 @@ let md5sum =
   if arch = "Darwin" then "md5 -q" else "md5sum"
 
 
-(** * md5sum command *)
-
-let md5sum =
-  if arch = "Darwin" then "md5 -q" else "md5sum"
-
-
 (** * Documentation : do we have latex, hevea, ... *)
 
 let check_doc () =
-- 
cgit v1.2.3