adds pushing of dev branch
authorChris Koeritz <fred@gruntose.com>
Tue, 16 Oct 2018 01:03:19 +0000 (01:03 +0000)
committerChris Koeritz <fred@gruntose.com>
Tue, 16 Oct 2018 01:03:19 +0000 (01:03 +0000)
commitc464ce977693edf72cdafaedbfd9aff8025557f8
tree976ce546fbaa5778865cef1a45889c9ae0dd2d76
parent3e92d9db9ab028fbb0d15915bff6e4514eb0a707
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.
scripts/rev_control/push_repo_downstream.sh