]> matita.cs.unibo.it Git - helm.git/blob - helm/ocaml/hbugs/scripts/sabba.sh
snapshot
[helm.git] / helm / ocaml / hbugs / scripts / sabba.sh
1 #!/bin/sh
2 # Copyright (C) 2003:
3 #    Stefano Zacchiroli <zack@cs.unibo.it>
4 #    for the HELM Team http://helm.cs.unibo.it/
5
6 #  This file is part of HELM, an Hypertextual, Electronic
7 #  Library of Mathematics, developed at the Computer Science
8 #  Department, University of Bologna, Italy.
9
10 #  HELM is free software; you can redistribute it and/or
11 #  modify it under the terms of the GNU General Public License
12 #  as published by the Free Software Foundation; either version 2
13 #  of the License, or (at your option) any later version.
14
15 #  HELM is distributed in the hope that it will be useful,
16 #  but WITHOUT ANY WARRANTY; without even the implied warranty of
17 #  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
18 #  GNU General Public License for more details.
19
20 #  You should have received a copy of the GNU General Public License
21 #  along with HELM; if not, write to the Free Software
22 #  Foundation, Inc., 59 Temple Place - Suite 330, Boston,
23 #  MA  02111-1307, USA.
24
25 #  For details, see the HELM World-Wide-Web page,
26 #  http://helm.cs.unibo.it/
27 if [ "$1" = "--help" -o "$1" = "" ]; then
28    echo "sabba.sh { start | stop | --help }"
29    exit 0
30 fi
31
32 ./scripts/ls_tutors.ml |
33 while read line; do
34    tutor=`echo $line | sed 's/\.ml//'`
35    if [ "$1" = "stop" ]; then
36       echo -n "Stopping HBugs tutor $tutor ... "
37       killall -9 $tutor
38       echo "done!"
39    elif [ "$1" = "start" ]; then
40       echo -n "Starting HBugs tutor $tutor ... "
41       nice -n 19 ./$tutor &> run/$tutor.log &
42       echo "done!"
43    else
44       echo "Uh? Try --help"
45       exit 1
46    fi
47 done