--- 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