diff options
| -rw-r--r-- | lang/ocaml/files/patch-configure | 11 |
1 files changed, 11 insertions, 0 deletions
diff --git a/lang/ocaml/files/patch-configure b/lang/ocaml/files/patch-configure index 527b978fc452..52225bc723ae 100644 --- a/lang/ocaml/files/patch-configure +++ b/lang/ocaml/files/patch-configure @@ -1,5 +1,16 @@ --- configure.orig 2014-10-03 19:25:46 UTC +++ configure +@@ -85,10 +85,6 @@ exec 3>&1 + + # Parse command-line arguments + +-if echo "$configure_options" | grep -q -e '--\?[a-zA-Z0-9-]\+='; then +- err "Arguments to this script look like '-prefix /foo/bar', not '-prefix=/foo/bar' (note the '=')." +-fi +- + while : ; do + case "$1" in + "") break;; @@ -659,7 +659,8 @@ if test $with_sharedlibs = "yes"; then mksharedlib="$flexlink" mkmaindll="$flexlink -maindll" |