diff -r 5b6cf0fbc329 -r 9df2f825422b README_REPOSITORY --- a/README_REPOSITORY Sun Dec 23 19:54:15 2012 +0100 +++ b/README_REPOSITORY Wed Dec 26 11:06:21 2012 +0100 @@ -141,27 +141,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. macbroy20 .. -macbroy29). You also need to be a member of the "isabelle" Unix -group. +with properly configured ssh to the local machines (e.g. lxbroy10). +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@macbroy20//home/isabelle-repository/repos/isabelle + hg out ssh://wenzelm@lxbroy10//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@macbroy20//home/isabelle-repository/repos/isabelle + hg push ssh://wenzelm@lxbroy10//home/isabelle-repository/repos/isabelle Default paths for push and pull can be configured in isabelle/.hg/hgrc, for example: [paths] - default = ssh://wenzelm@macbroy20//home/isabelle-repository/repos/isabelle + default = ssh://wenzelm@lxbroy10//home/isabelle-repository/repos/isabelle Now "hg pull" or "hg push" will use that shared file space, unless a different URL is specified explicitly. @@ -170,7 +169,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@macbroy20//home/isabelle-repository/repos/isabelle + hg clone ssh://wenzelm@lxbroy10//home/isabelle-repository/repos/isabelle Simple merges