diff options
| author | Guillaume Melquiond | 2015-08-17 16:02:35 +0200 |
|---|---|---|
| committer | Guillaume Melquiond | 2015-08-17 16:02:35 +0200 |
| commit | 369a0c9354497639d96ba2fef94c920e051d00fb (patch) | |
| tree | 9e5942f51e33524370efe9f610b4bc7497cc32ac | |
| parent | 45779d74209a728cfd67628eaa53b42fee129f65 (diff) | |
Remove duplicate code.
| -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 () = |