equal
deleted
inserted
replaced
73 The Munich site maintains an rsync server for the Isabelle |
73 The Munich site maintains an rsync server for the Isabelle |
74 distribution or website. |
74 distribution or website. |
75 |
75 |
76 The rsync tool is very smart and efficient in mirroring large |
76 The rsync tool is very smart and efficient in mirroring large |
77 directory hierarchies. See http://rsync.samba.org/ for more |
77 directory hierarchies. See http://rsync.samba.org/ for more |
78 information. The rsync-isabelle script provides a simple front-end |
78 information. The $PRG script provides a simple front-end |
79 for easy access to the Isabelle distribution. |
79 for easy access to the Isabelle distribution. |
80 |
80 |
81 The script can be either run in conservative or clean-sweep mode. |
81 The script can be either run in conservative or clean-sweep mode. |
82 |
82 |
83 1) Basic mirroring works like this: |
83 1) Basic mirroring works like this: |
106 like this: |
106 like this: |
107 |
107 |
108 $PRG -d /foo/bar |
108 $PRG -d /foo/bar |
109 |
109 |
110 |
110 |
111 After gaining some confidence in the workings of rsync-isabelle one |
111 After gaining some confidence in the workings of $PRG one |
112 would usually set up some automatic mirror scheme, e.g. a daily cron |
112 would usually set up some automatic mirror scheme, e.g. a daily cron |
113 job run by the 'nobody' user. |
113 job run by the 'nobody' user. |
114 |
114 |
115 Add -w to the option list in order to mirror the whole Isabelle website |
115 Add -w to the option list in order to mirror the whole Isabelle website |
116 |
116 |