only make development snapshots for successful tests
authorkleing
Fri May 09 14:15:50 2003 +0200 (2003-05-09)
changeset 1399388a8911bb65d
parent 13992 93769c6c85d7
child 13994 aa78df2e254b
only make development snapshots for successful tests
Admin/isatest-check
Admin/isatest-makedist
     1.1 --- a/Admin/isatest-check	Fri May 09 14:08:04 2003 +0200
     1.2 +++ b/Admin/isatest-check	Fri May 09 14:15:50 2003 +0200
     1.3 @@ -4,7 +4,8 @@
     1.4  # Author: Gerwin Klein, TU Muenchen
     1.5  # License: GPL (GNU GENERAL PUBLIC LICENSE)
     1.6  #
     1.7 -# DESCRIPTION: sends email for failed tests (checks for error.log)
     1.8 +# DESCRIPTION: sends email for failed tests, checks for error.log,
     1.9 +#              generates development snapshot if test ok
    1.10  
    1.11  # source bashrc, we're called by cron
    1.12  . ~/.bashrc
    1.13 @@ -20,11 +21,15 @@
    1.14  # canoncical home for all platforms
    1.15  HOME=/usr/stud/isatest
    1.16  
    1.17 +# where to find the distribution
    1.18 +DISTPREFIX=$HOME/isadist
    1.19 +
    1.20  # mail program
    1.21  MAIL=$HOME/bin/pmail
    1.22  
    1.23 -# where the error log is
    1.24 +# where the logs are
    1.25  ERRORLOG=$HOME/var/error.log
    1.26 +MASTERLOG=$HOME/log/isatest.log
    1.27  
    1.28  # where the test-still-running files are
    1.29  RUNNING=$HOME/var/running
    1.30 @@ -42,7 +47,8 @@
    1.31    echo
    1.32    echo "Usage: $PRG"
    1.33    echo
    1.34 -  echo "   sends email for failed tests, checks for error.log."
    1.35 +  echo "   sends email for failed tests, checks for error.log,"
    1.36 +  echo "   generates development snapshot if test ok."
    1.37    echo "   To be called by cron."
    1.38    echo
    1.39    exit 1
    1.40 @@ -91,5 +97,9 @@
    1.41      exit 1
    1.42  fi
    1.43  
    1.44 +# generate development snapshot page only for successful tests
    1.45 +(cd $HOME/devel-page; env DISTNAME=`$DISTPREFIX/Isabelle/bin/isatool version` make)
    1.46 +echo "$(date) $HOSTNAME $PRG: generated development snapshot web page." >> $MASTERLOG
    1.47 +
    1.48  exit 0
    1.49  ## end
     2.1 --- a/Admin/isatest-makedist	Fri May 09 14:08:04 2003 +0200
     2.2 +++ b/Admin/isatest-makedist	Fri May 09 14:15:50 2003 +0200
     2.3 @@ -92,9 +92,6 @@
     2.4  cd $DISTPREFIX >> $DISTLOG 2>&1
     2.5  $TAR xvzf `cat $DISTPREFIX/ISABELLE_DIST` >> $DISTLOG 2>&1
     2.6  
     2.7 -echo "### generating development snapshot web page" >> $DISTLOG 2>&1
     2.8 -(cd $HOME/devel-page; make)
     2.9 -
    2.10  echo ------------------- prepared test successfully --- `date` --- $HOSTNAME >> $DISTLOG 2>&1
    2.11  gzip -f $DISTLOG
    2.12