isabelle: Admin/isatest-settings@ba05effdec42 (annotated)

16615 e665dafdd2b8 use global settings for isatest-doc kleing parents: 16106 diff changeset	1	# -- shell-script --
16095 f6af6b265d20 put global isatest settings in one file, sourced by the other scripts kleing parents: diff changeset	2	# $Id$
f6af6b265d20 put global isatest settings in one file, sourced by the other scripts kleing parents: diff changeset	3	# Author: Gerwin Klein, NICTA
f6af6b265d20 put global isatest settings in one file, sourced by the other scripts kleing parents: diff changeset	4	#
f6af6b265d20 put global isatest settings in one file, sourced by the other scripts kleing parents: diff changeset	5	# DESCRIPTION: common settings for the isatest-* scripts
f6af6b265d20 put global isatest settings in one file, sourced by the other scripts kleing parents: diff changeset	6
f6af6b265d20 put global isatest settings in one file, sourced by the other scripts kleing parents: diff changeset	7	# source bashrc, we're called by cron
f6af6b265d20 put global isatest settings in one file, sourced by the other scripts kleing parents: diff changeset	8	. ~/.bashrc
f6af6b265d20 put global isatest settings in one file, sourced by the other scripts kleing parents: diff changeset	9
f6af6b265d20 put global isatest settings in one file, sourced by the other scripts kleing parents: diff changeset	10	# canoncical home for all platforms
16106 c2ea4b171f99 path /home/stud doesn't exist on macbroy33 (only /usr/stud) kleing parents: 16095 diff changeset	11	HOME=/usr/stud/isatest
16095 f6af6b265d20 put global isatest settings in one file, sourced by the other scripts kleing parents: diff changeset	12
f6af6b265d20 put global isatest settings in one file, sourced by the other scripts kleing parents: diff changeset	13	## send email on failure to
16616 491d8dbdb3b8 use kleing@cse instead of kleing@in.tum.de kleing parents: 16615 diff changeset	14	MAILTO="kleing@cse.unsw.edu.au nipkow@in.tum.de berghofe@in.tum.de schirmer@in.tum.de lp15@cam.ac.uk skalberg@in.tum.de makarius@sketis.net haftmann@in.tum.de"
16095 f6af6b265d20 put global isatest settings in one file, sourced by the other scripts kleing parents: diff changeset	15
f6af6b265d20 put global isatest settings in one file, sourced by the other scripts kleing parents: diff changeset	16	LOGPREFIX=$HOME/log
f6af6b265d20 put global isatest settings in one file, sourced by the other scripts kleing parents: diff changeset	17	MASTERLOG=$LOGPREFIX/isatest.log
f6af6b265d20 put global isatest settings in one file, sourced by the other scripts kleing parents: diff changeset	18
f6af6b265d20 put global isatest settings in one file, sourced by the other scripts kleing parents: diff changeset	19	ERRORDIR=$HOME/var
f6af6b265d20 put global isatest settings in one file, sourced by the other scripts kleing parents: diff changeset	20	ERRORLOG=$ERRORDIR/error.log
f6af6b265d20 put global isatest settings in one file, sourced by the other scripts kleing parents: diff changeset	21
f6af6b265d20 put global isatest settings in one file, sourced by the other scripts kleing parents: diff changeset	22	RUNNING=$HOME/var/running
f6af6b265d20 put global isatest settings in one file, sourced by the other scripts kleing parents: diff changeset	23
f6af6b265d20 put global isatest settings in one file, sourced by the other scripts kleing parents: diff changeset	24	DISTPREFIX=$HOME/tmp/isadist

author	wenzelm
	Thu, 28 Jul 2005 15:20:00 +0200
changeset 16943	ba05effdec42
parent 16616	491d8dbdb3b8
child 17446	f869b73b71ec
permissions	-rw-r--r--