author | wenzelm |
Wed, 01 Mar 2000 16:40:14 +0100 | |
changeset 8323 | 64b67ed25a59 |
parent 8322 | 6ba8356baa34 |
child 8324 | df7dccddc3de |
Admin/mirror-dist | file | annotate | diff | comparison | revisions |
--- a/Admin/mirror-dist Wed Mar 01 16:39:17 2000 +0100 +++ b/Admin/mirror-dist Wed Mar 01 16:40:14 2000 +0100 @@ -6,13 +6,15 @@ HOST=$(hostname) case ${HOST} in + sunbroy79) + #test + DEST=/tmp/isabelle-dist + mkdir -p $DEST + ;; *.cl.cam.ac.uk) USER=paulson DEST=/anfs/www/html/Research/HVG/Isabelle/dist ;; - sunbroy79) - DEST=/tmp/isabelle-dist - ;; *) echo "Unknown destination directory for ${HOST}" exit 2