diff --git a/configure b/configure index facc07de07c..d7df45e42e0 100755 --- a/configure +++ b/configure @@ -4836,7 +4836,7 @@ fi BINDINGS_TO_BUILD="" case "$enableval" in - all | yes | default | auto) BINDINGS_TO_BUILD="auto" ;; + yes | default | auto) BINDINGS_TO_BUILD="auto" ;; all ) BINDINGS_TO_BUILD="ocaml" ;; none | no) BINDINGS_TO_BUILD="" ;; *)for a_binding in `echo $enableval|sed -e 's/,/ /g' ` ; do