refer to $PRG instead of (old) rsync-isabelle;
authorwenzelm
Thu, 29 Sep 2005 19:37:20 +0200
changeset 17728 1412f84c420a
parent 17727 83d64a461507
child 17729 d74d0b5052a0
refer to $PRG instead of (old) rsync-isabelle;
Admin/isasync
--- a/Admin/isasync	Thu Sep 29 18:01:12 2005 +0200
+++ b/Admin/isasync	Thu Sep 29 19:37:20 2005 +0200
@@ -75,7 +75,7 @@
 
 The rsync tool is very smart and efficient in mirroring large
 directory hierarchies.  See http://rsync.samba.org/ for more
-information.  The rsync-isabelle script provides a simple front-end
+information.  The $PRG script provides a simple front-end
 for easy access to the Isabelle distribution.
 
 The script can be either run in conservative or clean-sweep mode.
@@ -108,7 +108,7 @@
   $PRG -d /foo/bar
 
 
-After gaining some confidence in the workings of rsync-isabelle one
+After gaining some confidence in the workings of $PRG one
 would usually set up some automatic mirror scheme, e.g. a daily cron
 job run by the 'nobody' user.