# HG changeset patch
# User wenzelm
# Date 951925139 -3600
# Node ID dc13f558856ddb792eb3189bf4eff1f35434cea3
# Parent  073144bed7da17e66f5d9948630794b5f9f5a6f7
tuned;

diff -r 073144bed7da -r dc13f558856d Admin/mirror-main
--- a/Admin/mirror-main	Wed Mar 01 15:00:21 2000 +0100
+++ b/Admin/mirror-main	Wed Mar 01 16:38:59 2000 +0100
@@ -3,7 +3,9 @@
 # $Id$
 #
 
-case $(hostname) in
+HOST=$(hostname)
+
+case ${HOST} in
   sunbroy30)
     DEST=/home/html/isabelle/html-data
     ;;
@@ -12,7 +14,7 @@
     DEST=/anfs/www/html/Research/HVG/Isabelle
     ;;
   *)
-    echo "Unknown destination directory for $(hostname)!"
+    echo "Unknown destination directory for ${HOST}"
     exit 2
     ;;
 esac