author | wenzelm |
Wed, 01 Mar 2000 16:38:59 +0100 | |
changeset 8321 | dc13f558856d |
parent 8320 | 073144bed7da |
child 8322 | 6ba8356baa34 |
Admin/mirror-main | file | annotate | diff | comparison | revisions |
--- 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