diff options
| author | Pierre | 2014-01-08 10:34:27 +0100 |
|---|---|---|
| committer | Matthieu Sozeau | 2014-05-06 09:58:55 +0200 |
| commit | 757b85ea8e208cf9f58985ed1acaef2cdc8037eb (patch) | |
| tree | 287422b9b44532f36be944df4084175364e1177c | |
| parent | be030aef23a094aff85de6066cb97d5c110d56ae (diff) | |
md5 for MacOS
md5sum check remains not portable.
| -rw-r--r-- | configure.ml | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/configure.ml b/configure.ml index db82e523c9..7cb37e82c1 100644 --- a/configure.ml +++ b/configure.ml @@ -785,6 +785,12 @@ 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 () = |