aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
-rw-r--r--configure.ml3
1 files changed, 2 insertions, 1 deletions
diff --git a/configure.ml b/configure.ml
index 6748da1d8..5b4ab883d 100644
--- a/configure.ml
+++ b/configure.ml
@@ -827,7 +827,8 @@ let strip =
(** * md5sum command *)
let md5sum =
- if arch = "Darwin" || arch = "FreeBSD" then "md5 -q" else "md5sum"
+ if List.mem arch ["Darwin"; "FreeBSD"; "OpenBSD"]
+ then "md5 -q" else "md5sum"
(** * Documentation : do we have latex, hevea, ... *)