isabelle: Admin/isatest-settings@967a3c7fd1f6 (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
19941 f0aeb6a145b1 new standard dir structure kleing parents: 17446 diff changeset	11	HOME=/home/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
17446 f869b73b71ec tuned; wenzelm parents: 16616 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 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	webertj
	Tue, 01 Aug 2006 15:28:55 +0200
changeset 20277	967a3c7fd1f6
parent 19941	f0aeb6a145b1
permissions	-rw-r--r--