equal
deleted
inserted
replaced
53 echo "### cleaning up old dist directory" >> $DISTLOG 2>&1 |
53 echo "### cleaning up old dist directory" >> $DISTLOG 2>&1 |
54 rm -rf $DISTPREFIX >> $DISTLOG 2>&1 |
54 rm -rf $DISTPREFIX >> $DISTLOG 2>&1 |
55 |
55 |
56 echo "### cleaning up old isabelle-* directories" >> $DISTLOG 2>&1 |
56 echo "### cleaning up old isabelle-* directories" >> $DISTLOG 2>&1 |
57 rm -rf $HOME/isabelle-* |
57 rm -rf $HOME/isabelle-* |
58 ssh atbroy102 "rm -rf isabelle-cygwin-poly" |
58 ssh atbroy102 "rm -rf /home/isatest/isabelle-cygwin-poly" |
59 |
59 |
60 echo "### building distribution" >> $DISTLOG 2>&1 |
60 echo "### building distribution" >> $DISTLOG 2>&1 |
61 mkdir -p $DISTPREFIX |
61 mkdir -p $DISTPREFIX |
62 $MAKEDIST >> $DISTLOG 2>&1 |
62 $MAKEDIST >> $DISTLOG 2>&1 |
63 |
63 |
79 exit 1 |
79 exit 1 |
80 fi |
80 fi |
81 |
81 |
82 cd $DISTPREFIX >> $DISTLOG 2>&1 |
82 cd $DISTPREFIX >> $DISTLOG 2>&1 |
83 $TAR xvzf `cat $DISTPREFIX/ISABELLE_DIST` >> $DISTLOG 2>&1 |
83 $TAR xvzf `cat $DISTPREFIX/ISABELLE_DIST` >> $DISTLOG 2>&1 |
|
84 |
|
85 ssh atbroy102 "rm -rf /home/isatest/isadist && mkdir -p /home/isatest/isadist" && \ |
|
86 rsync -a "$HOME/isadist/." atbroy102:/home/isatest/isadist/. |
84 |
87 |
85 echo ------------------- prepared test successfully --- `date` --- $HOSTNAME >> $DISTLOG 2>&1 |
88 echo ------------------- prepared test successfully --- `date` --- $HOSTNAME >> $DISTLOG 2>&1 |
86 |
89 |
87 ELAPSED=$("$HOME/bin/showtime" "$SECONDS") |
90 ELAPSED=$("$HOME/bin/showtime" "$SECONDS") |
88 log "dist build successful, elapsed time $ELAPSED." |
91 log "dist build successful, elapsed time $ELAPSED." |