--- a/Admin/mirror-website Wed May 12 13:52:34 2010 +0200 +++ b/Admin/mirror-website Wed May 12 13:54:49 2010 +0200 @@ -1,7 +1,5 @@ #!/usr/bin/env bash # -# $Id$ -# # mirrors the Isabelle website HOST=$(hostname)