.sshconfig: set gerrit port

diff --git a/.ssh/config b/.ssh/config
index 50096473fe593cf3d33992272cddca3af7784d95..681592182a19c890cb3eb811a33a053e2d98f310 100644 (file)
--- a/.ssh/config
+++ b/.ssh/config
@@ -90,6 +90,7 @@ Host gerrit.chromium.org
        Port 29418
        IdentityFile ~/.ssh/id_rsa.google
 Host gerrit-int.chromium.org git.chromium.org review.source.android.com review.coreboot.org
+       Port 29419
        IdentityFile ~/.ssh/id_rsa.google
 
 Host work