diff options
Diffstat (limited to 'scripts/get_compute_library.sh')
| -rwxr-xr-x | scripts/get_compute_library.sh | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/scripts/get_compute_library.sh b/scripts/get_compute_library.sh index 8d6fb2aaf3..6385011780 100755 --- a/scripts/get_compute_library.sh +++ b/scripts/get_compute_library.sh @@ -46,6 +46,9 @@ done DIR="$( cd -P "$( dirname "$SRC" )" >/dev/null && pwd )" pushd ${DIR} > /dev/null cd ../.. +if [ -z "$USERNAME" ]; then + USERNAME=$USER +fi if [ -z "$GITHUB_USERNAME" ]; then GITHUB_USERNAME=$USERNAME echo "setting GITHUB_USERNAME: ${GITHUB_USERNAME} use -g command line option to change" |