1 #!/usr/bin/env bash
2 #
3 # $Id$
4 #
5 # mirrors the Isabelle website
3 # mirrors the Isabelle website
6
4
7 HOST=$(hostname)
5 HOST=$(hostname)
8