# HG changeset patch
# User wenzelm
# Date 1354183019 -3600
# Node ID cbba160847842a31e7bf17e3f4bdf7e630aea35b
# Parent  0eb9b5d09f31fc682441ead2188d91bf3eed356c
further update and clarification of the all-important README_REPOSITORY;

diff -r 0eb9b5d09f31 -r cbba16084784 README_REPOSITORY
--- a/README_REPOSITORY	Thu Nov 29 10:45:25 2012 +0100
+++ b/README_REPOSITORY	Thu Nov 29 10:56:59 2012 +0100
@@ -22,6 +22,12 @@
 
     ./isabelle/bin/isabelle jedit
 
+4. For later update replace "hg clone ..." above by:
+
+    cd isabelle
+
+    hg pull -u
+
 
 Introduction
 ------------
@@ -189,11 +195,18 @@
   * Start publishing again by pull or fetch, which normally produces
     local merges.
 
-  * Test the merged result as usual and push back in real time.
+  * Test the merged result, e.g. like this:
+
+      isabelle build -a
+
+  * Push back in real time.
 
 Piling private changes and public merges longer than 0.5-2 hours is
 apt to produce some mess when pushing eventually!
 
+The pull-test-push cycle should not be repeated too fast, to avoid
+delaying others from doing the same concurrently.
+
 
 Content discipline
 ------------------