diff -r b7e7557e80b5 -r 0351cc781a26 README_REPOSITORY
--- a/README_REPOSITORY	Thu Jan 31 22:21:05 2013 +0100
+++ b/README_REPOSITORY	Fri Feb 01 21:31:21 2013 +0100
@@ -138,26 +138,26 @@
 time of writing and many years later.
 
 Push access to the Isabelle repository requires an account at TUM,
-with properly configured ssh to the local machines (e.g. lxbroy10).
-You also need to be a member of the "isabelle" Unix group.
+with properly configured ssh to isabelle-server.in.tum.de.  You also
+need to be a member of the "isabelle" Unix group.
 
 Sharing a locally modified clone then works as follows, using your
 user name instead of "wenzelm":
 
-  hg out ssh://wenzelm@lxbroy10//home/isabelle-repository/repos/isabelle
+  hg out ssh://wenzelm@isabelle-server.in.tum.de//home/isabelle-repository/repos/isabelle
 
 In fact, the "out" or "outgoing" command performs only a dry run: it
 displays the changesets that would get published.  An actual "push",
 with a lasting effect on the Isabelle repository, works like this:
 
-  hg push ssh://wenzelm@lxbroy10//home/isabelle-repository/repos/isabelle
+  hg push ssh://wenzelm@isabelle-server.in.tum.de//home/isabelle-repository/repos/isabelle
 
 
 Default paths for push and pull can be configured in
 isabelle/.hg/hgrc, for example:
 
   [paths]
-  default = ssh://wenzelm@lxbroy10//home/isabelle-repository/repos/isabelle
+  default = ssh://wenzelm@isabelle-server.in.tum.de//home/isabelle-repository/repos/isabelle
 
 Now "hg pull" or "hg push" will use that shared file space, unless a
 different URL is specified explicitly.
@@ -166,7 +166,7 @@
 source URL.  So we could have cloned via that ssh URL in the first
 place, to get exactly to the same point:
 
-  hg clone ssh://wenzelm@lxbroy10//home/isabelle-repository/repos/isabelle
+  hg clone ssh://wenzelm@isabelle-server.in.tum.de//home/isabelle-repository/repos/isabelle
 
 
 Simple merges