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.

2 files changed, 47 insertions, 0 deletions

diff --git a/scripts/git/git-pull-all.sh b/scripts/git/git-pull-all.sh
index 7f82eda296..52a5c6140c 100755
--- a/scripts/git/git-pull-all.sh
+++ b/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
 
diff --git a/scripts/git/git-setup-dirs.sh b/scripts/git/git-setup-dirs.sh
index 1f61eb8b83..3cc184dafb 100755
--- a/scripts/git/git-setup-dirs.sh
+++ b/scripts/git/git-setup-dirs.sh
@@ -40,6 +40,10 @@ function usage()
   echo "       (current: $GITHUB_PULL)"
   echo "   TOR_GITHUB_PUSH: the tor-github remote push URL"
   echo "       (current: $GITHUB_PUSH)"
+  echo "   TOR_GITLAB_PULL: the tor-gitlab remote pull URL"
+  echo "       (current: $GITLAB_PULL)"
+  echo "   TOR_GITLAB_PUSH: the tor-gitlab remote push URL"
+  echo "       (current: $GITLAB_PUSH)"
   echo "   TOR_EXTRA_CLONE_ARGS: extra arguments to git clone"
   echo "       (current: $TOR_EXTRA_CLONE_ARGS)"
   echo "   TOR_EXTRA_REMOTE_NAME: the name of an extra remote"
@@ -83,6 +87,10 @@ fi
 GITHUB_PULL=${TOR_GITHUB_PULL:-"https://github.com/torproject/tor.git"}
 GITHUB_PUSH=${TOR_GITHUB_PUSH:-"No_Pushing_To_GitHub"}
 
+# GitLab repositories
+GITLAB_PULL=${TOR_GITLAB_PULL:-"https://gitlab.torproject.org/tpo/core/tor.git"}
+GITLAB_PUSH=${TOR_GITLAB_PUSH:-"No_Pushing_To_GitLab"}
+
 ##########################
 # Git branches to manage #
 ##########################
@@ -343,6 +351,20 @@ function set_tor_github_pr_fetch_config
     "refs/pull.*pr"
 }
 
+# Set up the tor-github PR config, so tor-gitlab/mr/NNNN points to GitHub
+# MR NNNN. In some repositories, "/head" is optional.
+function set_tor_gitlab_mr_fetch_config
+{
+  # standard branches
+  replace_fetch_config tor-gitlab \
+    "+refs/heads/*:refs/remotes/tor-gitlab/*" \
+    "refs/heads"
+  # MRs
+  replace_fetch_config tor-gitlab \
+    "+refs/merge-requests/*/head:refs/remotes/tor-gitlab/mr/*" \
+    "refs/merge-requests.*mr"
+}
+
 # Add a new worktree for branch at path.
 # If the directory already exists: fail if $USE_EXISTING is 0, otherwise skip.
 function add_worktree
@@ -471,6 +493,15 @@ set_tor_github_pr_fetch_config
 # Now fetch them all
 fetch_remote "tor-github"
 
+# GitLab remote
+printf "%s Seting up remote %s\\n" "$MARKER" "${BYEL}tor-gitlab${CNRM}"
+add_remote "tor-gitlab" "$GITLAB_PULL"
+set_remote_push "tor-gitlab" "$GITLAB_PUSH"
+# Add custom fetch for MRs
+set_tor_gitlab_mr_fetch_config
+# Now fetch them all
+fetch_remote "tor-gitlab"
+
 # Extra remote
 if [ "$TOR_EXTRA_REMOTE_NAME" ]; then
   printf "%s Setting up remote %s\\n" "$MARKER" \