Merge changes from github.
Change: 138675832
diff --git a/util/python/python_config.sh b/util/python/python_config.sh
index 8a780c8..789c4b3 100755
--- a/util/python/python_config.sh
+++ b/util/python/python_config.sh
@@ -120,20 +120,28 @@
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