Admin/rsync-isabelle
changeset 8545 263a30b90c16
parent 8544 edaac961e181
child 8546 dc053bc2ea06
equal deleted inserted replaced
8544:edaac961e181 8545:263a30b90c16
     1 #!/bin/sh
     1 #!/bin/sh
     2 #
     2 #
     3 # mirror script for isabelle distribution
     3 # mirror script for Isabelle distribution
     4 #
     4 #
     5 # $Id$
     5 # $Id$
     6 #
     6 #
     7 
     7 
     8 ## diagnostics
     8 ## diagnostics