Mercurial Mercurial > repos > isabelle / annotate
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Admin/isatest/isatest-settings
author Andreas Lochbihler
Wed, 30 May 2012 16:05:21 +0200
changeset 48042 918a92d4079f
parent 47707 7a316fef84a4
child 48147 a29f3f44e198
permissions -rw-r--r--
merged
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
31310
b5365a9db718 uniform treatment of shellscript mode;
wenzelm
parents: 29926
diff changeset 
     1
 
# -*- shell-script -*- :mode=shellscript:
31582
4753c317d5c1 eliminated cvs ids;
wenzelm
parents: 31310
diff changeset 
     2
 
#
22410
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset 
     3
 
# Author: Gerwin Klein, NICTA
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset 
     4
 
#
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset 
     5
 
# DESCRIPTION: common settings for the isatest-* scripts
da313b67a04d moved all isatest/cron job related files to own directory
kleing
parents:
diff changeset 
     6
 












da313b67a04d
moved all isatest/cron job related files to own directory



kleing


parents: 

diff
changeset




     7


# source bashrc, we're called by cron













da313b67a04d
moved all isatest/cron job related files to own directory



kleing


parents: 

diff
changeset




     8


. ~/.bashrc













da313b67a04d
moved all isatest/cron job related files to own directory



kleing


parents: 

diff
changeset




     9














da313b67a04d
moved all isatest/cron job related files to own directory



kleing


parents: 

diff
changeset




    10


# canoncical home for all platforms













da313b67a04d
moved all isatest/cron job related files to own directory



kleing


parents: 

diff
changeset




    11


HOME=/home/isatest













da313b67a04d
moved all isatest/cron job related files to own directory



kleing


parents: 

diff
changeset




    12














da313b67a04d
moved all isatest/cron job related files to own directory



kleing


parents: 

diff
changeset




    13


## send email on failure to








38250






b32a44361186
added Lars Noschinski to isatest report



haftmann


parents: 
37834

diff
changeset




    14


MAILTO="\













b32a44361186
added Lars Noschinski to isatest report



haftmann


parents: 
37834

diff
changeset




    15


kleing@cse.unsw.edu.au \













b32a44361186
added Lars Noschinski to isatest report



haftmann


parents: 
37834

diff
changeset




    16


nipkow@in.tum.de \













b32a44361186
added Lars Noschinski to isatest report



haftmann


parents: 
37834

diff
changeset




    17


berghofe@in.tum.de \













b32a44361186
added Lars Noschinski to isatest report



haftmann


parents: 
37834

diff
changeset




    18


lp15@cam.ac.uk \













b32a44361186
added Lars Noschinski to isatest report



haftmann


parents: 
37834

diff
changeset




    19


makarius@sketis.net \













b32a44361186
added Lars Noschinski to isatest report



haftmann


parents: 
37834

diff
changeset




    20


blanchet@in.tum.de \













b32a44361186
added Lars Noschinski to isatest report



haftmann


parents: 
37834

diff
changeset




    21


boehmes@in.tum.de \













b32a44361186
added Lars Noschinski to isatest report



haftmann


parents: 
37834

diff
changeset




    22


bulwahn@in.tum.de \













b32a44361186
added Lars Noschinski to isatest report



haftmann


parents: 
37834

diff
changeset




    23


hoelzl@in.tum.de \













b32a44361186
added Lars Noschinski to isatest report



haftmann


parents: 
37834

diff
changeset




    24


krauss@in.tum.de \








47103






187cac088582
more isatest subscribers;



wenzelm


parents: 
45908

diff
changeset




    25


noschinl@in.tum.de \








47309






9d02327ede56
added me to isatest email list



sultana


parents: 
47214

diff
changeset




    26


kuncar@in.tum.de \













9d02327ede56
added me to isatest email list



sultana


parents: 
47214

diff
changeset




    27


ns441@cam.ac.uk"








22410






da313b67a04d
moved all isatest/cron job related files to own directory



kleing


parents: 

diff
changeset




    28














da313b67a04d
moved all isatest/cron job related files to own directory



kleing


parents: 

diff
changeset




    29


LOGPREFIX=$HOME/log













da313b67a04d
moved all isatest/cron job related files to own directory



kleing


parents: 

diff
changeset




    30


MASTERLOG=$LOGPREFIX/isatest.log








37834






c78327288b50
use different log server (macbroy23 down)



kleing


parents: 
33467

diff
changeset




    31


LOGSERVER=macbroy28.informatik.tu-muenchen.de








22410






da313b67a04d
moved all isatest/cron job related files to own directory



kleing


parents: 

diff
changeset




    32














da313b67a04d
moved all isatest/cron job related files to own directory



kleing


parents: 

diff
changeset




    33


ERRORDIR=$HOME/var













da313b67a04d
moved all isatest/cron job related files to own directory



kleing


parents: 

diff
changeset




    34


ERRORLOG=$ERRORDIR/error.log













da313b67a04d
moved all isatest/cron job related files to own directory



kleing


parents: 

diff
changeset




    35














da313b67a04d
moved all isatest/cron job related files to own directory



kleing


parents: 

diff
changeset




    36


RUNNING=$HOME/var/running













da313b67a04d
moved all isatest/cron job related files to own directory



kleing


parents: 

diff
changeset




    37









28567






3caee0cd91d8
change DISTPREFIX to not use yet another filesystem



kleing


parents: 
28539

diff
changeset




    38


DISTPREFIX=$HOME/isadist








28539






bdb308737bfd
do logging to MASTERLOG centrally (avoid multiple writers over NFS as



kleing


parents: 
24782

diff
changeset




    39









45908






143d2514347f
enforce short hostname on all platforms (especially macbroy2);



wenzelm


parents: 
45253

diff
changeset




    40


HOSTNAME="$(hostname -s)"













143d2514347f
enforce short hostname on all platforms (especially macbroy2);



wenzelm


parents: 
45253

diff
changeset




    41









28539






bdb308737bfd
do logging to MASTERLOG centrally (avoid multiple writers over NFS as



kleing


parents: 
24782

diff
changeset




    42


# this function avoids NFS inconsistencies with multiple writers by













bdb308737bfd
do logging to MASTERLOG centrally (avoid multiple writers over NFS as



kleing


parents: 
24782

diff
changeset




    43


# sshing to one central machine and writing locally. There is stil a













bdb308737bfd
do logging to MASTERLOG centrally (avoid multiple writers over NFS as



kleing


parents: 
24782

diff
changeset




    44


# race condition, but at least it should not corrupt a whole set of entries













bdb308737bfd
do logging to MASTERLOG centrally (avoid multiple writers over NFS as



kleing


parents: 
24782

diff
changeset




    45


# any more.













bdb308737bfd
do logging to MASTERLOG centrally (avoid multiple writers over NFS as



kleing


parents: 
24782

diff
changeset




    46


function log()













bdb308737bfd
do logging to MASTERLOG centrally (avoid multiple writers over NFS as



kleing


parents: 
24782

diff
changeset




    47


{













bdb308737bfd
do logging to MASTERLOG centrally (avoid multiple writers over NFS as



kleing


parents: 
24782

diff
changeset




    48


  MSG="$1"













bdb308737bfd
do logging to MASTERLOG centrally (avoid multiple writers over NFS as



kleing


parents: 
24782

diff
changeset




    49


  TIMESTAMP="$(date)"













bdb308737bfd
do logging to MASTERLOG centrally (avoid multiple writers over NFS as



kleing


parents: 
24782

diff
changeset




    50


  echo "[$TIMESTAMP $HOSTNAME $PRG]: $MSG" | ssh $LOGSERVER "cat >> $MASTERLOG"








28567






3caee0cd91d8
change DISTPREFIX to not use yet another filesystem



kleing


parents: 
28539

diff
changeset




    51


}















isabelle