Update git scripts with gitlab support
Our scripts in scripts/git
set up a remote for the github repository, and set it up so that when you run git pull on that remote, you get all the github pull requests.
We should set up the same for our gitlab remote.
Additionally, we should consider updating push-all (or creating a new script) so that it can create a bunch of pull requests for a family of foo_{035,042,043...}
branches.
I'll have a go at this once tpo/tpa/gitlab#41 (closed) is done -- it's hard to test it before then.