Admin/mirror-website
changeset 36859 51af1657263b
parent 31086 3e69a25b90a2
equal deleted inserted replaced
36858:8eac822dec6c 36859:51af1657263b
     1 #!/usr/bin/env bash
     1 #!/usr/bin/env bash
     2 #
       
     3 # $Id$
       
     4 #
     2 #
     5 # mirrors the Isabelle website
     3 # mirrors the Isabelle website
     6 
     4 
     7 HOST=$(hostname)
     5 HOST=$(hostname)
     8 
     6