--- /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
+ 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:
+++ /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_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:
--- /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
+
+# 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
-
-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
-
--- /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/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
+
+++ /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/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
-
--- /dev/null
+#!/bin/sh
+#
+# init.d script for http_getter
+#
+# by --Zack <zack@cs.unibo.it>
+# 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
+
+++ /dev/null
-#!/bin/sh
-#
-# init.d script for http_getter
-#
-# by --Zack <zack@cs.unibo.it>
-# 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
-
--- /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: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
+
+++ /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: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
-
--- /dev/null
+#!/bin/sh
+#
+# init.d script for http_getter
+#
+# by --Zack <zack@cs.unibo.it>
+# 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
+
+++ /dev/null
-#!/bin/sh
-#
-# init.d script for http_getter
-#
-# by --Zack <zack@cs.unibo.it>
-# 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
-
--- /dev/null
+#!/bin/sh
+#
+# init.d script for HELM searchEngine
+#
+# by --Zack <zack@cs.unibo.it>
+# 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
+
+++ /dev/null
-#!/bin/sh
-#
-# init.d script for HELM searchEngine
-#
-# by --Zack <zack@cs.unibo.it>
-# 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
-
+++ /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=""
-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
-
--- /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: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
+
+++ /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: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
-
--- /dev/null
+#!/bin/sh
+#
+# init.d script for http_getter
+#
+# by --Zack <zack@cs.unibo.it>
+# 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
+
--- /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=""
+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
+
+++ /dev/null
-#!/bin/sh
-#
-# init.d script for http_getter
-#
-# by --Zack <zack@cs.unibo.it>
-# 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
-
+++ /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_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
-
# 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"
# start uwobo
start_uwobo ()
{
- /etc/init.d/helm-uwobo_mowgli start &
+ /etc/init.d/helm-uwobo start &
}
# first check
projects / helm.git / commitdiff