Admin/mirror-dist
changeset 8397 f2d371bde3c4
parent 8396 16f6de8c897b
child 8398 f1c80ed70f48
     1.1 --- a/Admin/mirror-dist	Thu Mar 09 17:19:49 2000 +0100
     1.2 +++ b/Admin/mirror-dist	Thu Mar 09 17:25:28 2000 +0100
     1.3 @@ -6,7 +6,7 @@
     1.4  HOST=$(hostname)
     1.5  
     1.6  case  ${HOST} in
     1.7 -  sunbroy79)
     1.8 +  sunbroy*)
     1.9      #test
    1.10      DEST=/tmp/isabelle-dist
    1.11      mkdir -p $DEST
    1.12 @@ -20,4 +20,4 @@
    1.13      ;;
    1.14  esac
    1.15  
    1.16 -mirror-isabelle-dist -d $DEST
    1.17 +exec $(dirname $0)/mirror-isabelle-dist -d $DEST