Update git scripts to include tor-gitlab repository

Analogously to tor-github, we now make a tor-gitlab repository. It is set up to disable push direct attempts, and to fetch merge requests into appropriate branches.

git-pull-all.sh knows how to fetch this repository.