[mike@mwxm4]

mgshrc.example

@@ -26,8 +26,13 @@ gitpath     = /home/git
 # and visibility. <name> is yours to pick and becomes the git remote created in
 # the repository, so `git push gitlab` keeps working outside mgsh.
 #
-# `pushremote` pushes to every configured server in the order given,
-# `pushremote @gitlab` to a single one.
+# `pushremote` pushes to every active server in the order given,
+# `pushremote @gitlab` to a single one (active or not).
+#
+# `deleteremote @gitlab` (or `deleteremote gitlab.example.com`) deletes the
+# project's repository there again, after asking. It always needs the server
+# named, and the token needs permission to delete: delete_repo on GitHub,
+# write:repository on Gitea, api + Owner on GitLab.
 #
 # remote.gitea.url         = https://git.example.com
 # remote.gitea.key         = <personal-access-token>
@@ -38,6 +43,8 @@ gitpath     = /home/git
 # remote.gitlab.key        = <personal-access-token>
 # remote.gitlab.type       = gitlab
 # remote.gitlab.visibility = public
+# remote.gitlab.active     = false     # default true; false = only used when
+#                                      # named, e.g. `pushremote @gitlab`
 #
 # remotes          = gitea, gitlab   # optional: restrict and order the set
 # mirror           = true            # `push` also mirrors via pushremote