diff options
| -rwxr-xr-x | tool/git-refresh | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/tool/git-refresh b/tool/git-refresh index 48096fde36..2ee5bbfa39 100755 --- a/tool/git-refresh +++ b/tool/git-refresh @@ -33,10 +33,10 @@ if [ -d "$dir" ]; then echo updating `expr "/$dir/" : '.*/\([^/][^/]*\)/'` ... [ $quiet ] || set -x $CHDIR "$dir" - git fetch "$@" - exec git checkout ${branch:+"$branch"} "$@" + ${branch:+git fetch "$@"} + exec git ${branch:+checkout} "${branch:-pull}" "$@" else echo retrieving `expr "/$dir/" : '.*/\([^/][^/]*\)/'` ... [ $quiet ] || set -x - exec git clone "$url" "$dir" "$@" + exec git clone ${branch:+--branch "$branch"} "$url" "$dir" "$@" fi |