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