equal
deleted
inserted
replaced
90 fi |
90 fi |
91 |
91 |
92 cd $DISTPREFIX >> $DISTLOG 2>&1 |
92 cd $DISTPREFIX >> $DISTLOG 2>&1 |
93 $TAR xvzf `cat $DISTPREFIX/ISABELLE_DIST` >> $DISTLOG 2>&1 |
93 $TAR xvzf `cat $DISTPREFIX/ISABELLE_DIST` >> $DISTLOG 2>&1 |
94 |
94 |
95 echo "### generating development snapshot web page" >> $DISTLOG 2>&1 |
|
96 (cd $HOME/devel-page; make) |
|
97 |
|
98 echo ------------------- prepared test successfully --- `date` --- $HOSTNAME >> $DISTLOG 2>&1 |
95 echo ------------------- prepared test successfully --- `date` --- $HOSTNAME >> $DISTLOG 2>&1 |
99 gzip -f $DISTLOG |
96 gzip -f $DISTLOG |
100 |
97 |
101 ELAPSED=$("$HOME/bin/showtime" "$SECONDS") |
98 ELAPSED=$("$HOME/bin/showtime" "$SECONDS") |
102 echo "$(date) $HOSTNAME $PRG: dist build successful, elapsed time $ELAPSED." >> $MASTERLOG |
99 echo "$(date) $HOSTNAME $PRG: dist build successful, elapsed time $ELAPSED." >> $MASTERLOG |