diff options
| -rw-r--r-- | configure.ml | 6 |
1 files changed, 0 insertions, 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 () = |