Since gitlab.torproject.org is accessible from outside the internal
network, it can be removed from ssh jump host configuration.

doc/ssh-jump-host.md

@@ -8,12 +8,12 @@ If you have a recent enough ssh (>= 2016 or so), then you can use the `ProxyJump
 
 With recent ssh versions:
 
-    Host *.torproject.org !people.torproject.org
+    Host *.torproject.org !people.torproject.org !gitlab.torproject.org
       ProxyJump people.torproject.org
 
 Or with old ssh versions (before OpenSSH 7.3, or Debian 10 "buster"):
 
-    Host *.torproject.org !people.torproject.org
+    Host *.torproject.org !people.torproject.org !gitlab.torproject.org
       ProxyCommand ssh -l %r -W %h:%p people.torproject.org
 
 If your local username is different from your TPO username, also set