Index: tools/cr/cr-bash-helpers.sh |
diff --git a/tools/cr/cr-bash-helpers.sh b/tools/cr/cr-bash-helpers.sh |
index f80377156edab8212fa7956fccf615ce70f8a954..66a2de6c1752ea1f2b999aa64cb9744ac77f9472 100755 |
--- a/tools/cr/cr-bash-helpers.sh |
+++ b/tools/cr/cr-bash-helpers.sh |
@@ -14,8 +14,12 @@ if [[ -n "$BASH_VERSION" && "${BASH_SOURCE:-$0}" == "$0" ]]; then |
exit 1 |
fi |
+READLINK_e="readlink -e" |
+if [[ -x `which greadlink` ]]; then |
+ READLINK_e="greadlink -e" |
bulach
2014/02/04 05:51:25
nit: unindent (as 13-14 above)
Jeffrey Yasskin
2014/02/04 06:59:03
Oops, fixed.
|
+fi |
-cr_base_dir=$(dirname $(realpath "${BASH_SOURCE:-$0}")) |
+cr_base_dir=$(dirname $($READLINK_e "${BASH_SOURCE:-$0}")) |
cr_main="${cr_base_dir}/main.py" |
cr_exec=("PYTHONDONTWRITEBYTECODE=1" "python" "${cr_main}") |