From: Stefano Zacchiroli Date: Fri, 16 Apr 2004 16:16:01 +0000 (+0000) Subject: removed tedious "_mowgli" postfix X-Git-Tag: dead_dir_walking~49 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=cbcedd8ea841d69bf2f743730c0d4d511bbcb58c;p=helm.git removed tedious "_mowgli" postfix --- diff --git a/helm/scripts/init.d/etc_default_helm b/helm/scripts/init.d/etc_default_helm new file mode 100644 index 000000000..b284b5dd3 --- /dev/null +++ b/helm/scripts/init.d/etc_default_helm @@ -0,0 +1,35 @@ +# 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 + helm-search-engine + helm-uwobo + helm-rdfly +" + + # script used to load/unload uwobo predefined scripts +UWOBO_INIT_SCRIPT="/projects/helm/etc/init.d/loadPredefinedStylesheets.pl" + + # http getter cache dirs that need to be created at boot time +HTTP_GETTER_CACHE_DIRS=" + /tmp/helm + /tmp/helm/cache + /tmp/helm/cache/cic_library + /tmp/helm/cache/rdf_library + /tmp/helm/cache/nuprl_library +" + + # user which will own the daemons and the cache directories +OWNER="sacerdot:helm" + +export HELM_GETTER_URL=http://mowgli.cs.unibo.it:58081 +export HELM_UWOBO_URL=http://mowgli.cs.unibo.it:58080 +UWOBO_PANEL_CONF=/projects/helm/public_html/uwobo/panel/control.html +NUPRL_UWOBO_PANEL_CONF="/projects/helm/nuprl/NuPRL/uwobo-panel/control.html" + +# vim: set ft=sh: diff --git a/helm/scripts/init.d/etc_default_helm_mowgli b/helm/scripts/init.d/etc_default_helm_mowgli deleted file mode 100644 index 64ced1a28..000000000 --- a/helm/scripts/init.d/etc_default_helm_mowgli +++ /dev/null @@ -1,35 +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_mowgli - helm-proof-checker_mowgli - helm-uri-set-queue_mowgli - helm-draw-graph_mowgli - helm-search-engine_mowgli - helm-uwobo_mowgli - helm-rdfly_mowgli -" - - # script used to load/unload uwobo predefined scripts -UWOBO_INIT_SCRIPT="/projects/helm/etc/init.d/loadPredefinedStylesheets.pl" - - # http getter cache dirs that need to be created at boot time -HTTP_GETTER_CACHE_DIRS=" - /tmp/helm - /tmp/helm/cache - /tmp/helm/cache/cic_library - /tmp/helm/cache/rdf_library - /tmp/helm/cache/nuprl_library -" - - # user which will own the daemons and the cache directories -OWNER="sacerdot:helm" - -export HELM_GETTER_URL=http://mowgli.cs.unibo.it:58081 -export HELM_UWOBO_URL=http://mowgli.cs.unibo.it:58080 -UWOBO_PANEL_CONF=/projects/helm/public_html/uwobo/panel/control.html -NUPRL_UWOBO_PANEL_CONF="/projects/helm/nuprl/NuPRL/uwobo-panel/control.html" - -# vim: set ft=sh: diff --git a/helm/scripts/init.d/helm b/helm/scripts/init.d/helm new file mode 100755 index 000000000..c58a15d50 --- /dev/null +++ b/helm/scripts/init.d/helm @@ -0,0 +1,37 @@ +#!/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 new file mode 100755 index 000000000..37decf723 --- /dev/null +++ b/helm/scripts/init.d/helm-bootmisc.sh @@ -0,0 +1,16 @@ +#!/bin/sh + +HTTP_GETTER_CACHE_DIRS="" +if [ -f /etc/default/helm ]; then + . /etc/default/helm +fi + +# 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-bootmisc_mowgli.sh b/helm/scripts/init.d/helm-bootmisc_mowgli.sh deleted file mode 100755 index fc24432d2..000000000 --- a/helm/scripts/init.d/helm-bootmisc_mowgli.sh +++ /dev/null @@ -1,19 +0,0 @@ -#!/bin/sh - -HTTP_GETTER_CACHE_DIRS="" -if [ -f /etc/default/helm_mowgli ]; then - . /etc/default/helm_mowgli -fi - -# clean pid file for helm related daemons -( cd /var/run/ && rm -f *_mowgli.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 new file mode 100755 index 000000000..70859c08d --- /dev/null +++ b/helm/scripts/init.d/helm-draw-graph @@ -0,0 +1,53 @@ +#!/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/daemons/graphs/tools/drawGraph.opt +USAGE="Usage: /etc/init.d/helm-draw-graph { start | stop | restart }" + +if [ -f /etc/default/helm ]; then + . /etc/default/helm +fi + +NAME=`basename $DAEMON` +PIDFILE=/var/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-draw-graph_mowgli b/helm/scripts/init.d/helm-draw-graph_mowgli deleted file mode 100755 index a8553fb10..000000000 --- a/helm/scripts/init.d/helm-draw-graph_mowgli +++ /dev/null @@ -1,53 +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/daemons/graphs/tools/drawGraph.opt -USAGE="Usage: /etc/init.d/helm-draw-graph_mowgli { start | stop | restart }" - -if [ -f /etc/default/helm_mowgli ]; then - . /etc/default/helm_mowgli -fi - -NAME=`basename $DAEMON` -PIDFILE=/var/run/"$NAME"_mowgli.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 new file mode 100755 index 000000000..e1a7061d8 --- /dev/null +++ b/helm/scripts/init.d/helm-http-getter @@ -0,0 +1,53 @@ +#!/bin/sh +# +# init.d script for http_getter +# +# by --Zack +# Created: Tue, 8 Oct 2002 17:18:17 +0200 +# Last-Modified: Wed, 8 Jan 2003 12:09:41 +0100 + +DAEMON="/projects/helm/daemons/http_getter/http_getter.opt" +USAGE="Usage: /etc/init.d/helm-http-getter { start | stop | restart }" + +if [ -f /etc/default/helm ]; then + . /etc/default/helm +fi + +NAME=`basename $DAEMON` +PIDFILE=/var/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_mowgli b/helm/scripts/init.d/helm-http-getter_mowgli deleted file mode 100755 index 3ac21e0fa..000000000 --- a/helm/scripts/init.d/helm-http-getter_mowgli +++ /dev/null @@ -1,53 +0,0 @@ -#!/bin/sh -# -# init.d script for http_getter -# -# by --Zack -# Created: Tue, 8 Oct 2002 17:18:17 +0200 -# Last-Modified: Wed, 8 Jan 2003 12:09:41 +0100 - -DAEMON="/projects/helm/daemons/http_getter/http_getter.opt" -USAGE="Usage: /etc/init.d/helm-http-getter_mowgli { start | stop | restart }" - -if [ -f /etc/default/helm_mowgli ]; then - . /etc/default/helm_mowgli -fi - -NAME=`basename $DAEMON` -PIDFILE=/var/run/"$NAME"_mowgli.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 new file mode 100755 index 000000000..9ea0eaffc --- /dev/null +++ b/helm/scripts/init.d/helm-proof-checker @@ -0,0 +1,53 @@ +#!/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:39 +0100 + +DAEMON=/projects/helm/daemons/proofChecker/proofChecker.opt +USAGE="Usage: /etc/init.d/helm-proof-checker { start | stop | restart }" + +if [ -f /etc/default/helm ]; then + . /etc/default/helm +fi + +NAME=`basename $DAEMON` +PIDFILE=/var/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_mowgli b/helm/scripts/init.d/helm-proof-checker_mowgli deleted file mode 100755 index 8d28c9bf5..000000000 --- a/helm/scripts/init.d/helm-proof-checker_mowgli +++ /dev/null @@ -1,53 +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:39 +0100 - -DAEMON=/projects/helm/daemons/proofChecker/proofChecker.opt -USAGE="Usage: /etc/init.d/helm-proof-checker { start | stop | restart }" - -if [ -f /etc/default/helm_mowgli ]; then - . /etc/default/helm_mowgli -fi - -NAME=`basename $DAEMON` -PIDFILE=/var/run/"$NAME"_mowgli.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-rdfly b/helm/scripts/init.d/helm-rdfly new file mode 100755 index 000000000..ef17cd239 --- /dev/null +++ b/helm/scripts/init.d/helm-rdfly @@ -0,0 +1,53 @@ +#!/bin/sh +# +# init.d script for http_getter +# +# by --Zack +# Created: Tue, 8 Oct 2002 17:18:17 +0200 +# Last-Modified: Wed, 8 Jan 2003 12:09:41 +0100 + +DAEMON="/projects/helm/daemons/rdfly/rdfly.opt" +USAGE="Usage: /etc/init.d/helm-rdfly { start | stop | restart }" + +if [ -f /etc/default/helm ]; then + . /etc/default/helm +fi + +NAME=`basename $DAEMON` +PIDFILE=/var/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-rdfly_mowgli b/helm/scripts/init.d/helm-rdfly_mowgli deleted file mode 100755 index 5ff1e67ec..000000000 --- a/helm/scripts/init.d/helm-rdfly_mowgli +++ /dev/null @@ -1,53 +0,0 @@ -#!/bin/sh -# -# init.d script for http_getter -# -# by --Zack -# Created: Tue, 8 Oct 2002 17:18:17 +0200 -# Last-Modified: Wed, 8 Jan 2003 12:09:41 +0100 - -DAEMON="/projects/helm/daemons/rdfly/rdfly.opt" -USAGE="Usage: /etc/init.d/helm-rdfly_mowgli { start | stop | restart }" - -if [ -f /etc/default/helm_mowgli ]; then - . /etc/default/helm_mowgli -fi - -NAME=`basename $DAEMON` -PIDFILE=/var/run/"$NAME"_mowgli.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-search-engine b/helm/scripts/init.d/helm-search-engine new file mode 100755 index 000000000..6b9582cb2 --- /dev/null +++ b/helm/scripts/init.d/helm-search-engine @@ -0,0 +1,55 @@ +#!/bin/sh +# +# init.d script for HELM searchEngine +# +# by --Zack +# Created: Fri, 22 Nov 2002 15:51:25 +0100 +# Last-Modified: Thu, 6 Mar 2003 17:40:16 +0100 + +DAEMON="/projects/helm/daemons/searchEngine/searchEngine.opt" +USAGE="Usage: /etc/init.d/helm-search-engine { start | stop | restart }" + +if [ -f /etc/default/helm ]; then + . /etc/default/helm +fi + +NAME=`basename $DAEMON` +PIDFILE=/var/run/$NAME.pid + +do_start () { + echo -n "Starting $DAEMON ... " + start-stop-daemon \ + --start --pidfile $PIDFILE --make-pidfile \ + --chuid $OWNER --background --exec $DAEMON + echo "done!" +} + +do_stop () { + echo -n "Stopping $DAEMON ... " + start-stop-daemon --stop --pidfile $PIDFILE && \ + (if [ -f $PIDFILE ]; then rm -f $PIDFILE; else true; fi) + echo "done!" +} + +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-search-engine_mowgli b/helm/scripts/init.d/helm-search-engine_mowgli deleted file mode 100755 index 45ea7f885..000000000 --- a/helm/scripts/init.d/helm-search-engine_mowgli +++ /dev/null @@ -1,55 +0,0 @@ -#!/bin/sh -# -# init.d script for HELM searchEngine -# -# by --Zack -# Created: Fri, 22 Nov 2002 15:51:25 +0100 -# Last-Modified: Thu, 6 Mar 2003 17:40:16 +0100 - -DAEMON="/projects/helm/daemons/searchEngine/searchEngine.opt" -USAGE="Usage: /etc/init.d/helm-search-engine_mowgli { start | stop | restart }" - -if [ -f /etc/default/helm_mowgli ]; then - . /etc/default/helm_mowgli -fi - -NAME=`basename $DAEMON` -PIDFILE=/var/run/"$NAME"_mowgli.pid - -do_start () { - echo -n "Starting $DAEMON ... " - start-stop-daemon \ - --start --pidfile $PIDFILE --make-pidfile \ - --chuid $OWNER --background --exec $DAEMON - echo "done!" -} - -do_stop () { - echo -n "Stopping $DAEMON ... " - start-stop-daemon --stop --pidfile $PIDFILE && \ - (if [ -f $PIDFILE ]; then rm -f $PIDFILE; else true; fi) - echo "done!" -} - -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_mowgli b/helm/scripts/init.d/helm-tomcat_mowgli deleted file mode 100755 index 73cf5211c..000000000 --- a/helm/scripts/init.d/helm-tomcat_mowgli +++ /dev/null @@ -1,51 +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="" -if [ -f /etc/default/helm_mowgli ]; then - . /etc/default/helm_mowgli -fi -test -x "$UWOBO_INIT_SCRIPT" || exit 0 - -case "$1" in - - start) - echo -n "Loading UWOBO stylesheets (mowgli) ... " - $UWOBO_INIT_SCRIPT $UWOBO_PANEL_CONF > /dev/null - echo "done!" - echo -n "Loading UWOBO stylesheets (mowgli NuPRL) ... " - $UWOBO_INIT_SCRIPT $NUPRL_UWOBO_PANEL_CONF > /dev/null - echo "done!" - ;; - - stop) - $UWOBO_INIT_SCRIPT --unload $UWOBO_PANEL_CONF > /dev/null - $UWOBO_INIT_SCRIPT --unload $NUPRL_UWOBO_PANEL_CONF > /dev/null - ;; - - reload) - $UWOBO_INIT_SCRIPT --reload $UWOBO_PANEL_CONF > /dev/null - $UWOBO_INIT_SCRIPT --reload $NUPRL_UWOBO_PANEL_CONF > /dev/null - ;; - - restart) - $UWOBO_INIT_SCRIPT --unload $UWOBO_PANEL_CONF > /dev/null - $UWOBO_INIT_SCRIPT --unload $NUPRL_UWOBO_PANEL_CONF > /dev/null - $UWOBO_INIT_SCRIPT $UWOBO_PANEL_CONF > /dev/null - $UWOBO_INIT_SCRIPT $NUPRL_UWOBO_PANEL_CONF > /dev/null - ;; - - *) - echo - echo "Usage: /etc/init.d/helm-tomcat_mowgli { 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 new file mode 100755 index 000000000..415abdee6 --- /dev/null +++ b/helm/scripts/init.d/helm-uri-set-queue @@ -0,0 +1,53 @@ +#!/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:25 +0100 + +DAEMON=/projects/helm/daemons/graphs/tools/uriSetQueue.opt +USAGE="Usage: /etc/init.d/helm-uri-set-queue { start | stop | restart }" + +if [ -f /etc/default/helm ]; then + . /etc/default/helm +fi + +NAME=`basename $DAEMON` +PIDFILE=/var/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-uri-set-queue_mowgli b/helm/scripts/init.d/helm-uri-set-queue_mowgli deleted file mode 100755 index a1a069fcc..000000000 --- a/helm/scripts/init.d/helm-uri-set-queue_mowgli +++ /dev/null @@ -1,53 +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:25 +0100 - -DAEMON=/projects/helm/daemons/graphs/tools/uriSetQueue.opt -USAGE="Usage: /etc/init.d/helm-uri-set-queue_mowgli { start | stop | restart }" - -if [ -f /etc/default/helm_mowgli ]; then - . /etc/default/helm_mowgli -fi - -NAME=`basename $DAEMON` -PIDFILE=/var/run/"$NAME"_mowgli.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-uwobo b/helm/scripts/init.d/helm-uwobo new file mode 100755 index 000000000..94dfbe6e1 --- /dev/null +++ b/helm/scripts/init.d/helm-uwobo @@ -0,0 +1,67 @@ +#!/bin/sh +# +# init.d script for http_getter +# +# by --Zack +# Created: Wed, 15 Jan 2003 15:14:07 +0100 +# Last-Modified: Fri, 16 Apr 2004 17:54:54 +0200 + +DAEMON="/projects/helm/daemons/uwobo/uwobo.opt" +USAGE="Usage: /etc/init.d/helm-uwobo { start | stop | restart }" + +if [ -f /etc/default/helm ]; then + . /etc/default/helm +fi + +NAME=`basename $DAEMON` +# Warning: $PIDFILE value is shared by UWOBO respawner, change at your own risk +PIDFILE=/var/run/$NAME.pid + +do_start () { + echo -n "Starting $DAEMON ... " + start-stop-daemon \ + --start --background --pidfile $PIDFILE --make-pidfile \ + --chuid $OWNER --exec $DAEMON + echo "done!" + echo -n "Waiting for UWOBO to startup (2 seconds) ... " + sleep 2 + echo "done!" + /etc/init.d/helm-uwobo-stylesheets start + echo -n "Starting $DAEMON respawner" + /etc/init.d/daemon_respawner.sh -p $PIDFILE \ -m root@localhost \ + -r http://localhost:58080/help -d `basename $0` & + echo "." +} + +do_stop () { + echo -n "Stopping $DAEMON respawner" + /etc/init.d/daemon_respawner.sh -d `basename $0` -s + echo "." + echo -n "Stopping $DAEMON ... " + start-stop-daemon --stop --pidfile $PIDFILE && \ + (if [ -f $PIDFILE ]; then rm -f $PIDFILE; else true; fi) + echo "done!" +} + +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-uwobo-stylesheets b/helm/scripts/init.d/helm-uwobo-stylesheets new file mode 100755 index 000000000..9c0201446 --- /dev/null +++ b/helm/scripts/init.d/helm-uwobo-stylesheets @@ -0,0 +1,51 @@ +#!/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="" +if [ -f /etc/default/helm ]; then + . /etc/default/helm +fi +test -x "$UWOBO_INIT_SCRIPT" || exit 0 + +case "$1" in + + start) + echo -n "Loading UWOBO stylesheets (mowgli) ... " + $UWOBO_INIT_SCRIPT $UWOBO_PANEL_CONF > /dev/null + echo "done!" + echo -n "Loading UWOBO stylesheets (mowgli NuPRL) ... " + $UWOBO_INIT_SCRIPT $NUPRL_UWOBO_PANEL_CONF > /dev/null + echo "done!" + ;; + + stop) + $UWOBO_INIT_SCRIPT --unload $UWOBO_PANEL_CONF > /dev/null + $UWOBO_INIT_SCRIPT --unload $NUPRL_UWOBO_PANEL_CONF > /dev/null + ;; + + reload) + $UWOBO_INIT_SCRIPT --reload $UWOBO_PANEL_CONF > /dev/null + $UWOBO_INIT_SCRIPT --reload $NUPRL_UWOBO_PANEL_CONF > /dev/null + ;; + + restart) + $UWOBO_INIT_SCRIPT --unload $UWOBO_PANEL_CONF > /dev/null + $UWOBO_INIT_SCRIPT --unload $NUPRL_UWOBO_PANEL_CONF > /dev/null + $UWOBO_INIT_SCRIPT $UWOBO_PANEL_CONF > /dev/null + $UWOBO_INIT_SCRIPT $NUPRL_UWOBO_PANEL_CONF > /dev/null + ;; + + *) + echo + echo "Usage: /etc/init.d/helm-uwobo-stylesheets { start | stop | restart | reload }" >&2 + echo + exit 1 + ;; + +esac + diff --git a/helm/scripts/init.d/helm-uwobo_mowgli b/helm/scripts/init.d/helm-uwobo_mowgli deleted file mode 100755 index bcdb46983..000000000 --- a/helm/scripts/init.d/helm-uwobo_mowgli +++ /dev/null @@ -1,67 +0,0 @@ -#!/bin/sh -# -# init.d script for http_getter -# -# by --Zack -# Created: Wed, 15 Jan 2003 15:14:07 +0100 -# Last-Modified: Fri, 16 Apr 2004 17:54:54 +0200 - -DAEMON="/projects/helm/daemons/uwobo/uwobo.opt" -USAGE="Usage: /etc/init.d/helm-uwobo_mowgli { start | stop | restart }" - -if [ -f /etc/default/helm_mowgli ]; then - . /etc/default/helm_mowgli -fi - -NAME=`basename $DAEMON` -# Warning: $PIDFILE value is shared by UWOBO respawner, change at your own risk -PIDFILE=/var/run/"$NAME"_mowgli.pid - -do_start () { - echo -n "Starting $DAEMON ... " - start-stop-daemon \ - --start --background --pidfile $PIDFILE --make-pidfile \ - --chuid $OWNER --exec $DAEMON - echo "done!" - echo -n "Waiting for UWOBO to startup (2 seconds) ... " - sleep 2 - echo "done!" - /etc/init.d/helm-tomcat_mowgli start - echo -n "Starting $DAEMON respawner" - /etc/init.d/daemon_respawner.sh -p $PIDFILE \ -m root@localhost \ - -r http://localhost:58080/help -d `basename $0` & - echo "." -} - -do_stop () { - echo -n "Stopping $DAEMON respawner" - /etc/init.d/daemon_respawner.sh -d `basename $0` -s - echo "." - echo -n "Stopping $DAEMON ... " - start-stop-daemon --stop --pidfile $PIDFILE && \ - (if [ -f $PIDFILE ]; then rm -f $PIDFILE; else true; fi) - echo "done!" -} - -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_mowgli b/helm/scripts/init.d/helm_mowgli deleted file mode 100755 index 710859892..000000000 --- a/helm/scripts/init.d/helm_mowgli +++ /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_mowgli ]; then - . /etc/default/helm_mowgli -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_mowgli" - echo - exit 1 - ;; - -esac - diff --git a/helm/scripts/init.d/uwobo_forever.sh b/helm/scripts/init.d/uwobo_forever.sh index a7985c464..3b8e5d2e8 100755 --- a/helm/scripts/init.d/uwobo_forever.sh +++ b/helm/scripts/init.d/uwobo_forever.sh @@ -14,7 +14,7 @@ exit 0 # Warning: $PIDFILE value is shared by UWOBO /etc/init.d script, change at your # own risk -PIDFILE="/var/run/uwobo.opt_mowgli.pid" +PIDFILE="/var/run/uwobo.opt.pid" MAILTO="root@mowgli.cs.unibo.it" INTERVAL="60" @@ -38,7 +38,7 @@ uwobo_is_alive () # start uwobo start_uwobo () { - /etc/init.d/helm-uwobo_mowgli start & + /etc/init.d/helm-uwobo start & } # first check