1#! /bin/sh 2# 3# Loop over a problem set. If 4# /usr/wiss/stenzg/home_sun/tmp/SUNHALLE_RESERVED exists, run on 5# sunhalle52-107, otherwise use all hosts. 6# 7 8MYHOME=/usr/gast/schulz/home_sun/ 9STENZHOME=/usr/gast/stenzg/home_sun/ 10 11#MYHOME=/home/schulz 12#STENZHOME=/home/schulz 13 14touch $MYHOME/dummy; 15 16while test -f $MYHOME/dummy; do 17 echo New iteration - checking for jobs 18 if test -f $MYHOME/distribute_jobs; then 19 for file in `cat $MYHOME/distribute_jobs`; do 20 echo Running on $file 21 if test -f $STENZHOME/tmp/SUNHALLE_RESERVED; then 22 distribute_eprover.awk $file 52 107; 23 else 24 distribute_eprover.awk $file; 25 fi; 26 done; 27 mv $MYHOME/distribute_jobs $MYHOME/distribute_jobs_done 28 if test -f $MYHOME/distribute_jobs_queued; then 29 mv $MYHOME/distribute_jobs_queued $MYHOME/distribute_jobs 30 fi; 31 else 32 if test -f $MYHOME/distribute_jobs_queued; then 33 mv $MYHOME/distribute_jobs_queued $MYHOME/distribute_jobs 34 else 35 echo Sleeping 36 sleep 300; 37 fi; 38 fi; 39done; 40