From 56b18cb9bde667b9a3b7e87abfbb87e1f1fa18e3 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Antoine=20Beaupr=C3=A9?= <anarcat@debian.org>
Date: Tue, 18 May 2021 14:02:18 -0400
Subject: [PATCH] add examples on how to run the magic program

---
 howto/gitlab.md | 23 +++++++++++++++++++++++
 1 file changed, 23 insertions(+)

diff --git a/howto/gitlab.md b/howto/gitlab.md
index 0ecb0380..d30a4d63 100644
--- a/howto/gitlab.md
+++ b/howto/gitlab.md
@@ -495,6 +495,29 @@ GitLab API, that is:
  3. change the default branch
  4. *then* `git push -d` to delete the old branch
 
+You should run the script with an account that has "Maintainer" or
+"Owner" access to GitLab, so that it can do the above GitLab API
+changes. You will then need to provide an [access token](https://gitlab.torproject.org/-/profile/personal_access_tokens) through
+the `GITLAB_PRIVATE_TOKEN` environment variable. So, for example, this
+will rename the `master` branch to `main` on the local and remote
+repos:
+
+    GITLAB_PRIVATE_TOKEN=REDACTED git-branch-rename-remote
+
+If you want to rename another branch or remote, you can specify those
+on the commandline as well. For example, this will rename the
+`develop` branch to `dev` on the `gitlab` remote:
+
+    GITLAB_PRIVATE_TOKEN=REDACTED git-branch-rename-remote --remote gitlab --from-branch develop --to-branch dev
+
+The command can also be used to fix *other* repositories so that they
+correctly rename their local branch too. In that case, the GitLab
+repository is already up to date, so there is no need for an access
+token, and just running this command will rename `master` to `main` on
+the local repo, including remote tracking branches:
+
+    git-branch-rename-remote
+
 However, there are a few extra steps and considerations to make when
 changing the name of a heavily used branch.
 
-- 
GitLab