much nicer now; supports a path to push upstream.

diff --git a/scripts/rev_control/push_repo_upstream.sh b/scripts/rev_control/push_repo_upstream.sh
index 3d69f95f63f6cec3c853e122c07091668d9938dd..6210277e7a3eeb29490f3e0bb42c371a3c56906c 100755 (executable)
--- a/scripts/rev_control/push_repo_upstream.sh
+++ b/scripts/rev_control/push_repo_upstream.sh
@@ -10,8 +10,13 @@
 # rats: how did i set up that archive?
 #       we need to have those steps someplace.
 
+dir="$1"; shift
+if [ -z "$dir" ]; then
+  dir=.
+fi
+
+pushd "$dir"
 git fetch upstream
 git merge upstream/master
-
 git push origin master
-
+popd