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.

scripts/git/git-pull-all.sh

@@ -181,6 +181,19 @@ function fetch_tor_github
   fi
 }
 
+# Fetch tor-gitlab pull requests. No arguments.
+function fetch_tor_gitlab
+{
+  local cmd="git fetch tor-gitlab"
+  printf "  %s Fetching tor-gitlab..." "$MARKER"
+  if [ $DRY_RUN -eq 0 ]; then
+    msg=$( eval "$cmd" 2>&1 )
+    validate_ret $? "$msg"
+  else
+    printf "\\n      %s\\n" "${IWTH}$cmd${CNRM}"
+  fi
+}
+
 ###############
 # Entry point #
 ###############
@@ -189,6 +202,9 @@ function fetch_tor_github
 goto_repo "$ORIGIN_PATH"
 fetch_tor_github
 
+# Then tor-gitlab
+fetch_tor_gitlab
+
 # Then, fetch the origin.
 fetch_origin