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