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