aboutsummaryrefslogtreecommitdiffhomepage
path: root/configure.ml
diff options
context:
space:
mode:
authorGravatar Guillaume Melquiond <guillaume.melquiond@inria.fr>2015-08-17 16:02:35 +0200
committerGravatar Guillaume Melquiond <guillaume.melquiond@inria.fr>2015-08-17 16:02:35 +0200
commit369a0c9354497639d96ba2fef94c920e051d00fb (patch)
tree9e5942f51e33524370efe9f610b4bc7497cc32ac /configure.ml
parent45779d74209a728cfd67628eaa53b42fee129f65 (diff)
Remove duplicate code.
Diffstat (limited to 'configure.ml')
-rw-r--r--configure.ml6
1 files changed, 0 insertions, 6 deletions
diff --git a/configure.ml b/configure.ml
index d509aa70e..3fe34d6ca 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 () =