adds pushing of dev branch

this makes my changes show up a lot more frequently at the downstream
repos, since we used to only be synching the master branch.

diff --git a/scripts/rev_control/push_repo_downstream.sh b/scripts/rev_control/push_repo_downstream.sh
index 50f8d80aa63f532851dc241ba241073c4e74753c..f12fc74080918d53cf90175c7cdcbf38fc9fe010 100644 (file)
--- a/scripts/rev_control/push_repo_downstream.sh
+++ b/scripts/rev_control/push_repo_downstream.sh
@@ -62,6 +62,10 @@ exit_on_error "running the git pull downstream master"
 git push --tags downstream master
 exit_on_error "running the git push downstream master"
 
+# do our dev branch also.
+git push --tags downstream dev
+continue_on_error "running the git push downstream dev: is there a dev branch?"
+
 popd &>/dev/null
 
 restore_terminal_title