Problem with dev.push()

[David Roe]

I'm getting an error when using dev.push() from sage, which executes

git push ssh://g...@trac.sagemath.org:2222/sage.git ticket/14304:u/roed/ticket/14304
Pushing to ssh://g...@trac.sagemath.org:2222/sage.git
ssh: connect to host trac.sagemath.org port 2222: Operation timed out
fatal: Could not read from remote repository.
Please make sure you have the correct access rights and the repository exists.

When I delete the :2222 and do
git push ssh://g...@trac.sagemath.org/sage.git ticket/14304:u/roed/ticket/14304

it works.

Did something change recently in the gitolite configuration?  This was working for me a couple days ago.

If so, we should update the dev scripts.
David