+++ /dev/null
-# 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:
+++ /dev/null
-#!/bin/sh
-#
-# init.d script for HELM daemons
-#
-# by --Zack <zack@cs.unibo.it>
-# 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
-
+++ /dev/null
-#!/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
-
+++ /dev/null
-#!/bin/sh
-#
-# init.d script for HELM draw_graph.cgi
-#
-# by --Zack <zack@cs.unibo.it>
-# 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
-
+++ /dev/null
-#!/bin/sh
-#
-# init.d script for http_getter.pl
-#
-# by --Zack <zack@cs.unibo.it>
-# 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
-
+++ /dev/null
-#!/bin/sh
-#
-# init.d script for HELM proof checker
-#
-# by --Zack <zack@cs.unibo.it>
-# 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
-
+++ /dev/null
-#!/bin/sh
-#
-# init.d script for HELM daemons
-#
-# by --Zack <zack@cs.unibo.it>
-# 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
-
+++ /dev/null
-#!/bin/sh
-#
-# init.d script for HELM uri_set_queue.cgi
-#
-# by --Zack <zack@cs.unibo.it>
-# 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
-
projects / helm.git / commitdiff