Admin/isatest/isatest-makedist
changeset 40739 9c84b562620d
parent 37874 954dc0c580bd
child 41599 16e290c668ea
     1.1 --- a/Admin/isatest/isatest-makedist	Fri Nov 26 15:49:59 2010 -0800
     1.2 +++ b/Admin/isatest/isatest-makedist	Sat Nov 27 11:51:05 2010 +0100
     1.3 @@ -80,7 +80,9 @@
     1.4  fi
     1.5  
     1.6  cd $DISTPREFIX >> $DISTLOG 2>&1
     1.7 -$TAR xvzf `cat $DISTPREFIX/ISABELLE_DIST` >> $DISTLOG 2>&1
     1.8 +ISABELLE_DIST=`cat $DISTPREFIX/ISABELLE_DIST`
     1.9 +$TAR xvzf $ISABELLE_DIST >> $DISTLOG 2>&1
    1.10 +ln -sf $(basename $ISABELLE_DIST .tar.gz) Isabelle
    1.11  
    1.12  ssh atbroy102 "rm -rf /home/isatest/isadist && mkdir -p /home/isatest/isadist" && \
    1.13  rsync -a "$HOME/isadist/." atbroy102:/home/isatest/isadist/.