equal
deleted
inserted
replaced
1 # -*- shell-script -*- |
|
2 # $Id$ |
|
3 # Author: Gerwin Klein, NICTA |
|
4 # |
|
5 # DESCRIPTION: common settings for the isatest-* scripts |
|
6 |
|
7 # source bashrc, we're called by cron |
|
8 . ~/.bashrc |
|
9 |
|
10 # canoncical home for all platforms |
|
11 HOME=/home/isatest |
|
12 |
|
13 ## send email on failure to |
|
14 MAILTO="kleing@cse.unsw.edu.au nipkow@in.tum.de berghofe@in.tum.de schirmer@in.tum.de lp15@cam.ac.uk makarius@sketis.net haftmann@in.tum.de" |
|
15 |
|
16 LOGPREFIX=$HOME/log |
|
17 MASTERLOG=$LOGPREFIX/isatest.log |
|
18 |
|
19 ERRORDIR=$HOME/var |
|
20 ERRORLOG=$ERRORDIR/error.log |
|
21 |
|
22 RUNNING=$HOME/var/running |
|
23 |
|
24 DISTPREFIX=$HOME/tmp/isadist |
|