diff options
| -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 () = |