From: Claudio Sacerdoti Coen Date: Mon, 19 Jan 2004 09:54:59 +0000 (+0000) Subject: No longer in use. X-Git-Tag: V_0_5_1_3~38 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=f607fe07cf39edce4989711614139e00148612dd;p=helm.git No longer in use. --- diff --git a/helm/scripts/init.d/etc_default_helm b/helm/scripts/init.d/etc_default_helm deleted file mode 100644 index 4d06f941f..000000000 --- a/helm/scripts/init.d/etc_default_helm +++ /dev/null @@ -1,29 +0,0 @@ -# Configuration for helm daemons - - # DAEMONS started/stopped/ecc. by /etc/init.d/helm, name listed here - # must correspond to scripts located in /etc/init.d -DAEMONS=" - helm-http-getter - helm-proof-checker - helm-uri-set-queue - helm-draw-graph -" - - # script used to define a good(TM) environment for daemons -ENVSCRIPT="/projects/helm/shared/scripts/phd.rc" - - # script used to load/unload uwobo predefined scripts -UWOBO_INIT_SCRIPT="/projects/helm/shared/scripts/init.d/loadPredefinedStylesheets.pl" - - # http getter cache dirs that need to be created at boot time -HTTP_GETTER_CACHE_DIRS=" - /projects/helm/shared/cache/library - /projects/helm/shared/cache/library/http_getter - /projects/helm/shared/cache/rdf_library - /projects/helm/shared/cache/rdf_library/http_getter -" - - # user which will own the daemons and the cache directories -OWNER="sacerdot:helm" - -# vim: set ft=sh: diff --git a/helm/scripts/init.d/helm b/helm/scripts/init.d/helm deleted file mode 100755 index c58a15d50..000000000 --- a/helm/scripts/init.d/helm +++ /dev/null @@ -1,37 +0,0 @@ -#!/bin/sh -# -# init.d script for HELM daemons -# -# by --Zack -# Created: Tue, 8 Oct 2002 17:18:17 +0200 -# Last-Modified: Tue, 8 Oct 2002 17:18:17 +0200 - -DAEMONS="" -if [ -f /etc/default/helm ]; then - . /etc/default/helm -fi - -case "$1" in - - start|stop|restart|force-reload|reload) - for d in $DAEMONS; do - /etc/init.d/$d $1 - done - ;; - - *) - echo - echo "Usage: /etc/init.d/helm { start | stop | restart | force-reload | reload }" >&2 - echo - if [ -z "$DAEMONS" ]; then - echo "Actually, no daemons are considered!" - else - echo "Actually, considered daemons are: $DAEMONS" - fi - echo "to change this setting see /etc/default/helm" - echo - exit 1 - ;; - -esac - diff --git a/helm/scripts/init.d/helm-bootmisc.sh b/helm/scripts/init.d/helm-bootmisc.sh deleted file mode 100755 index 79e3b69a7..000000000 --- a/helm/scripts/init.d/helm-bootmisc.sh +++ /dev/null @@ -1,19 +0,0 @@ -#!/bin/sh - -HTTP_GETTER_CACHE_DIRS="" -if [ -f /etc/default/helm ]; then - . /etc/default/helm -fi - -# clean pid file for helm related daemons -( cd /projects/helm/run/ && rm -f *.pid ) - -# create http_getter cache dirs -for d in $HTTP_GETTER_CACHE_DIRS; do - if ! [ -d $d ]; then - mkdir -m 2775 $d - OWNER=`echo -n $OWNER | sed -e 's/:/./'` - chown $OWNER $d - fi -done - diff --git a/helm/scripts/init.d/helm-draw-graph b/helm/scripts/init.d/helm-draw-graph deleted file mode 100755 index 34490799e..000000000 --- a/helm/scripts/init.d/helm-draw-graph +++ /dev/null @@ -1,60 +0,0 @@ -#!/bin/sh -# -# init.d script for HELM draw_graph.cgi -# -# by --Zack -# Created: Wed, 9 Oct 2002 11:12:01 +0200 -# Last-Modified: Wed, 9 Oct 2002 11:12:01 +0200 - -#DAEMON=/projects/helm/graphs/tools/draw_graph.cgi -DAEMON=/projects/helm/graphs/tools/drawGraph.opt -USAGE="Usage: /etc/init.d/helm-draw-graph { start | stop | restart }" - -ENVSCRIPT="" -if [ -f /etc/default/helm ]; then - . /etc/default/helm -fi -if ! [ -f "$ENVSCRIPT" ]; then - echo "Can't find environment script '$ENVSCRIPT'" - exit 1 -fi -. $ENVSCRIPT &> /dev/null - -NAME=`basename $DAEMON` -PIDFILE=/projects/helm/run/$NAME.pid - -do_start () { - echo "Starting $DAEMON ..." - start-stop-daemon \ - --start --background --pidfile $PIDFILE --make-pidfile \ - --chuid $OWNER --exec $DAEMON -} - -do_stop () { - echo "Stopping $DAEMON ..." - start-stop-daemon --stop --pidfile $PIDFILE && \ - (if [ -f $PIDFILE ]; then rm -f $PIDFILE; else true; fi) -} - -case "$1" in - - start) - do_start - ;; - - stop) - do_stop - ;; - - restart) - do_stop - do_start - ;; - - *) - echo "$USAGE" >&2 - exit 1 - ;; - -esac - diff --git a/helm/scripts/init.d/helm-http-getter b/helm/scripts/init.d/helm-http-getter deleted file mode 100755 index ac9c2cc0a..000000000 --- a/helm/scripts/init.d/helm-http-getter +++ /dev/null @@ -1,59 +0,0 @@ -#!/bin/sh -# -# init.d script for http_getter.pl -# -# by --Zack -# Created: Tue, 8 Oct 2002 17:18:17 +0200 -# Last-Modified: Tue, 8 Oct 2002 17:18:17 +0200 - -DAEMON=/projects/helm/http_getter/http_getter.pl -USAGE="Usage: /etc/init.d/helm-http-getter { start | stop | restart }" - -ENVSCRIPT="" -if [ -f /etc/default/helm ]; then - . /etc/default/helm -fi -if ! [ -f "$ENVSCRIPT" ]; then - echo "Can't find environment script '$ENVSCRIPT'" - exit 1 -fi -. $ENVSCRIPT &> /dev/null - -NAME=`basename $DAEMON` -PIDFILE=/projects/helm/run/$NAME.pid - -do_start () { - echo "Starting $DAEMON ..." - start-stop-daemon \ - --start --background --pidfile $PIDFILE --make-pidfile \ - --chuid $OWNER --exec $DAEMON -} - -do_stop () { - echo "Stopping $DAEMON ..." - start-stop-daemon --stop --pidfile $PIDFILE && \ - (if [ -f $PIDFILE ]; then rm -f $PIDFILE; else true; fi) -} - -case "$1" in - - start) - do_start - ;; - - stop) - do_stop - ;; - - restart) - do_stop - do_start - ;; - - *) - echo "$USAGE" >&2 - exit 1 - ;; - -esac - diff --git a/helm/scripts/init.d/helm-proof-checker b/helm/scripts/init.d/helm-proof-checker deleted file mode 100755 index f3acbc12a..000000000 --- a/helm/scripts/init.d/helm-proof-checker +++ /dev/null @@ -1,59 +0,0 @@ -#!/bin/sh -# -# init.d script for HELM proof checker -# -# by --Zack -# Created: Wed, 9 Oct 2002 11:12:01 +0200 -# Last-Modified: Wed, 13 Nov 2002 18:30:09 +0100 - -DAEMON=/projects/helm/proofChecker/proofChecker.opt -USAGE="Usage: /etc/init.d/helm-proof-checker { start | stop | restart }" - -ENVSCRIPT="" -if [ -f /etc/default/helm ]; then - . /etc/default/helm -fi -if ! [ -f "$ENVSCRIPT" ]; then - echo "Can't find environment script '$ENVSCRIPT'" - exit 1 -fi -. $ENVSCRIPT &> /dev/null - -NAME=`basename $DAEMON` -PIDFILE=/projects/helm/run/$NAME.pid - -do_start () { - echo "Starting $DAEMON ..." - start-stop-daemon \ - --start --background --pidfile $PIDFILE --make-pidfile \ - --chuid $OWNER --exec $DAEMON -} - -do_stop () { - echo "Stopping $DAEMON ..." - start-stop-daemon --stop --pidfile $PIDFILE && \ - (if [ -f $PIDFILE ]; then rm -f $PIDFILE; else true; fi) -} - -case "$1" in - - start) - do_start - ;; - - stop) - do_stop - ;; - - restart) - do_stop - do_start - ;; - - *) - echo "$USAGE" >&2 - exit 1 - ;; - -esac - diff --git a/helm/scripts/init.d/helm-tomcat b/helm/scripts/init.d/helm-tomcat deleted file mode 100755 index 166ab31b1..000000000 --- a/helm/scripts/init.d/helm-tomcat +++ /dev/null @@ -1,50 +0,0 @@ -#!/bin/sh -# -# init.d script for HELM daemons -# -# by --Zack -# Created: Wed, 9 Oct 2002 14:26:27 +0200 -# Last-Modified: Wed, 9 Oct 2002 14:26:27 +0200 - -UWOBO_INIT_SCRIPT="" -ENVSCRIPT="" -if [ -f /etc/default/helm ]; then - . /etc/default/helm -fi -test -x "$UWOBO_INIT_SCRIPT" || exit 0 -if ! [ -f "$ENVSCRIPT" ]; then - echo "Can't find environment script '$ENVSCRIPT'" - exit 1 -fi -. $ENVSCRIPT &> /dev/null - -case "$1" in - - start) - echo -n "Loading UWOBO stylesheets (helm) ... " - $UWOBO_INIT_SCRIPT > /dev/null - echo "done!" - ;; - - stop) - $UWOBO_INIT_SCRIPT --unload > /dev/null - ;; - - reload) - $UWOBO_INIT_SCRIPT --reload > /dev/null - ;; - - restart) - $UWOBO_INIT_SCRIPT --unload > /dev/null - $UWOBO_INIT_SCRIPT > /dev/null - ;; - - *) - echo - echo "Usage: /etc/init.d/helm-tomcat { start | stop | restart | reload }" >&2 - echo - exit 1 - ;; - -esac - diff --git a/helm/scripts/init.d/helm-uri-set-queue b/helm/scripts/init.d/helm-uri-set-queue deleted file mode 100755 index 242545a7b..000000000 --- a/helm/scripts/init.d/helm-uri-set-queue +++ /dev/null @@ -1,60 +0,0 @@ -#!/bin/sh -# -# init.d script for HELM uri_set_queue.cgi -# -# by --Zack -# Created: Tue, 8 Oct 2002 17:18:17 +0200 -# Last-Modified: Wed, 20 Nov 2002 10:50:14 +0100 - -#DAEMON=/projects/helm/graphs/tools/uri_set_queue.cgi -DAEMON=/projects/helm/graphs/tools/uriSetQueue.opt -USAGE="Usage: /etc/init.d/helm-uri-set-queue { start | stop | restart }" - -ENVSCRIPT="" -if [ -f /etc/default/helm ]; then - . /etc/default/helm -fi -if ! [ -f "$ENVSCRIPT" ]; then - echo "Can't find environment script '$ENVSCRIPT'" - exit 1 -fi -. $ENVSCRIPT &> /dev/null - -NAME=`basename $DAEMON` -PIDFILE=/projects/helm/run/$NAME.pid - -do_start () { - echo "Starting $DAEMON ..." - start-stop-daemon \ - --start --background --pidfile $PIDFILE --make-pidfile \ - --chuid $OWNER --exec $DAEMON -} - -do_stop () { - echo "Stopping $DAEMON ..." - start-stop-daemon --stop --pidfile $PIDFILE && \ - (if [ -f $PIDFILE ]; then rm -f $PIDFILE; else true; fi) -} - -case "$1" in - - start) - do_start - ;; - - stop) - do_stop - ;; - - restart) - do_stop - do_start - ;; - - *) - echo "$USAGE" >&2 - exit 1 - ;; - -esac -