1 files changed, 43 insertions, 0 deletions
diff --git a/tool/git-refresh b/tool/git-refresh
new file mode 100755
index 0000000000..7f5361a853
--- /dev/null
+++ b/tool/git-refresh
@@ -0,0 +1,43 @@
+#!/bin/sh
+set -e
+
+quiet=
+branch=
+OPT_SPEC="\
+${0##*/} [options] URL dir [options]
+--
+C=directory         Change directory
+q,quiet             Quiet
+b,branch=branch     Checkout branch
+"
+rev="$(echo "$OPT_SPEC" | git rev-parse --parseopt -- "$@")"
+status=$?
+eval "$rev"
+[ $status = 0 ] || exit $status
+
+until [ $# = 0 ]; do
+    case "$1" in
+	--) shift; break;;
+	-C) shift; cd "$1";;
+	-q) quiet=1;;
+	-b) shift; branch="$1";;
+	-*) echo "unknown option: $1" 1>&2; exit 1;;
+	*) break;;
+    esac
+    shift
+done
+
+url="$1"
+dir="$2"
+shift 2
+if [ -d "$dir" ]; then
+    echo updating "${dir#*/}" ...
+    [ $quiet ] || set -x
+    cd "$dir"
+    git fetch "$@"
+    exec git checkout ${branch:+"$branch"} "$@"
+else
+    echo retrieving "${dir#*/}" ...
+    [ $quiet ] || set -x
+    exec git clone "$url" "$dir" "$@"
+fi