Admin/isatest/isatest-settings

generate take_induct lemmas

+
−# -*- shell-script -*- :mode=shellscript:
+
−#
+
−# Author: Gerwin Klein, NICTA
+
−#
+
−# DESCRIPTION: common settings for the isatest-* scripts
+
−
+
−# source bashrc, we're called by cron
+
−. ~/.bashrc
+
−
+
−# canoncical home for all platforms
+
−HOME=/home/isatest
+
−
+
−## send email on failure to
+
−MAILTO="[e-mail] [e-mail] [e-mail] [e-mail] [e-mail] [e-mail] [e-mail] [e-mail] [e-mail] [e-mail] [e-mail] [e-mail]"
+
−
+
−LOGPREFIX=$HOME/log
+
−MASTERLOG=$LOGPREFIX/isatest.log
+
−LOGSERVER=macbroy23.informatik.tu-muenchen.de
+
−
+
−ERRORDIR=$HOME/var
+
−ERRORLOG=$ERRORDIR/error.log
+
−
+
−RUNNING=$HOME/var/running
+
−
+
−DISTPREFIX=$HOME/isadist
+
−
+
−# this function avoids NFS inconsistencies with multiple writers by
+
−# sshing to one central machine and writing locally. There is stil a
+
−# race condition, but at least it should not corrupt a whole set of entries
+
−# any more.
+
−function log()
+
−{
+
−  MSG="$1"
+
−  TIMESTAMP="$(date)"
+
−  echo "[$TIMESTAMP $HOSTNAME $PRG]: $MSG" | ssh $LOGSERVER "cat >> $MASTERLOG"
+
−}