Admin/isasync
changeset 17728 1412f84c420a
parent 17671 e9e341bc7d42
child 18214 857444b28267
--- 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.