diff options
Diffstat (limited to 'math/coq/files/patch-configure.ml')
| -rw-r--r-- | math/coq/files/patch-configure.ml | 11 |
1 files changed, 11 insertions, 0 deletions
diff --git a/math/coq/files/patch-configure.ml b/math/coq/files/patch-configure.ml new file mode 100644 index 000000000000..e31ec3317f4f --- /dev/null +++ b/math/coq/files/patch-configure.ml @@ -0,0 +1,11 @@ +--- configure.ml.orig 2016-01-20 16:52:18 UTC ++++ configure.ml +@@ -843,7 +843,7 @@ let strip = + (** * md5sum command *) + + let md5sum = +- if arch = "Darwin" then "md5 -q" else "md5sum" ++ if arch = "FreeBSD" then "md5 -q" else "md5sum" + + + (** * Documentation : do we have latex, hevea, ... *) |