Merge changes from github.

Change: 138675832

1 files changed, 18 insertions, 10 deletions

diff --git a/util/python/python_config.sh b/util/python/python_config.sh
index 8a780c82b8..789c4b35b3 100755
--- a/util/python/python_config.sh
+++ b/util/python/python_config.sh
@@ -120,20 +120,28 @@ function setup_python {
     IFS=','
     python_lib_path=($(python_path))
     unset IFS
-    echo "Found possible Python library paths:"
-    for x in "${python_lib_path[@]}"; do
-      echo "  $x"
-    done
-    set -- "${python_lib_path[@]}"
-    echo "Please input the desired Python library path to use.  Default is ["$1"]"
-    read b || true
-    if [ "$b" == "" ]; then
+
+    if [ 1 = "$USE_DEFAULT_PYTHON_LIB_PATH" ]; then
       PYTHON_LIB_PATH="$(default_python_path "${python_lib_path[0]}")"
-      echo $PYTHON_LIB_PATH
+      echo "Using python library path: $PYTHON_LIB_PATH"
+
     else
-      PYTHON_LIB_PATH="$b"
+      echo "Found possible Python library paths:"
+      for x in "${python_lib_path[@]}"; do
+        echo "  $x"
+      done
+      set -- "${python_lib_path[@]}"
+      echo "Please input the desired Python library path to use.  Default is ["$1"]"
+      read b || true
+      if [ "$b" == "" ]; then
+        PYTHON_LIB_PATH="$(default_python_path "${python_lib_path[0]}")"
+        echo "Using python library path: $PYTHON_LIB_PATH"
+      else
+        PYTHON_LIB_PATH="$b"
+      fi
     fi
   fi
+
   if test -d "$PYTHON_LIB_PATH" -a -x "$PYTHON_LIB_PATH"; then
     python_lib="$PYTHON_LIB_PATH"
   else