README_REPOSITORY
changeset 47449 5e1482296b12
parent 40601 021278fdd0a8
child 48497 ba61aceaa18a
equal deleted inserted replaced
47448:cd3d987e8e79 47449:5e1482296b12
    30 other operations are local to the user's repository clone.  This gives
    30 other operations are local to the user's repository clone.  This gives
    31 some freedom for experimentation without affecting anybody else.
    31 some freedom for experimentation without affecting anybody else.
    32 
    32 
    33 Mercurial provides nice web presentation of incoming changes with a
    33 Mercurial provides nice web presentation of incoming changes with a
    34 digest of log entries; this also includes RSS/Atom news feeds.  There
    34 digest of log entries; this also includes RSS/Atom news feeds.  There
    35 are add-on browsers, notably hgtk that is part of the TortoiseHg
    35 are add-on history browsers such as "hg view" and TortoiseHg.  Unlike
    36 distribution and works for generic Python/GTk platforms.  The
    36 the default web view, some of these tools help to inspect the semantic
    37 alternative "view" utility helps to inspect the semantic content of
    37 content of non-trivial merge nodes.
    38 merge nodes.
       
    39 
    38 
    40 
    39 
    41 Initial configuration
    40 Initial configuration
    42 ---------------------
    41 ---------------------
    43 
    42 
   105 hooked on the main repository is called to keep an eye on incoming
   104 hooked on the main repository is called to keep an eye on incoming
   106 changes.  In any case, changesets need to be understandable, at the
   105 changes.  In any case, changesets need to be understandable, at the
   107 time of writing and many years later.
   106 time of writing and many years later.
   108 
   107 
   109 Push access to the Isabelle repository requires an account at TUM,
   108 Push access to the Isabelle repository requires an account at TUM,
   110 with properly configured ssh to the local machines (e.g. macbroy20,
   109 with properly configured ssh to the local machines (e.g. macbroy20 ..
   111 atbroy100).  You also need to be a member of the "isabelle" Unix
   110 macbroy29).  You also need to be a member of the "isabelle" Unix
   112 group.
   111 group.
   113 
   112 
   114 Sharing a locally modified clone then works as follows, using your
   113 Sharing a locally modified clone then works as follows, using your
   115 user name instead of "wenzelm":
   114 user name instead of "wenzelm":
   116 
   115 
   117   hg out ssh://wenzelm@atbroy100//home/isabelle-repository/repos/isabelle
   116   hg out ssh://wenzelm@macbroy20//home/isabelle-repository/repos/isabelle
   118 
   117 
   119 In fact, the "out" or "outgoing" command performs only a dry run: it
   118 In fact, the "out" or "outgoing" command performs only a dry run: it
   120 displays the changesets that would get published.  An actual "push",
   119 displays the changesets that would get published.  An actual "push",
   121 with a lasting effect on the Isabelle repository, works like this:
   120 with a lasting effect on the Isabelle repository, works like this:
   122 
   121 
   123   hg push ssh://wenzelm@atbroy100//home/isabelle-repository/repos/isabelle
   122   hg push ssh://wenzelm@macbroy20//home/isabelle-repository/repos/isabelle
   124 
   123 
   125 
   124 
   126 Default paths for push and pull can be configured in
   125 Default paths for push and pull can be configured in
   127 isabelle/.hg/hgrc, for example:
   126 isabelle/.hg/hgrc, for example:
   128 
   127 
   129   [paths]
   128   [paths]
   130   default = ssh://wenzelm@atbroy100//home/isabelle-repository/repos/isabelle
   129   default = ssh://wenzelm@macbroy20//home/isabelle-repository/repos/isabelle
   131 
   130 
   132 Now "hg pull" or "hg push" will use that shared file space, unless a
   131 Now "hg pull" or "hg push" will use that shared file space, unless a
   133 different URL is specified explicitly.
   132 different URL is specified explicitly.
   134 
   133 
   135 When cloning a repository, the default path is set to the initial
   134 When cloning a repository, the default path is set to the initial
   136 source URL.  So we could have cloned via that ssh URL in the first
   135 source URL.  So we could have cloned via that ssh URL in the first
   137 place, to get exactly to the same point:
   136 place, to get exactly to the same point:
   138 
   137 
   139   hg clone ssh://wenzelm@atbroy100//home/isabelle-repository/repos/isabelle
   138   hg clone ssh://wenzelm@macbroy20//home/isabelle-repository/repos/isabelle
   140 
   139 
   141 
   140 
   142 Simple merges
   141 Simple merges
   143 -------------
   142 -------------
   144 
   143