Admin/mirror-dist
2002-09-18 kleing 2002-09-18 comments + usage
2002-01-11 wenzelm 2002-01-11 #!/usr/bin/env bash;
2000-11-28 wenzelm 2000-11-28 tuned;
2000-03-09 wenzelm 2000-03-09 renamed to rsync-isabelle;
2000-03-09 wenzelm 2000-03-09 tuned;
2000-03-09 kleing 2000-03-09 made rsync "official"
2000-03-06 wenzelm 2000-03-06 rsyncd setup; --delete mode (beware!);
2000-03-06 kleing 2000-03-06 switched to mirroring with rsync server
2000-03-01 wenzelm 2000-03-01 test setup;
2000-03-01 wenzelm 2000-03-01 proper setup;
2000-02-09 wenzelm 2000-02-09 mirror dist page;