From 1777211e04075fd37bcee56b79cfbedcb89d57eb Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Wed, 20 Nov 2002 16:34:22 +0000 Subject: [PATCH] - changed invoked daemons for proof checker, draw graph and uri set queue to ocaml ones - bugfix: use different pid files for old a new libraries daemons --- helm/scripts/init.d/helm-draw-graph | 3 ++- helm/scripts/init.d/helm-draw-graph_mowgli | 5 +++-- helm/scripts/init.d/helm-proof-checker | 4 ++-- helm/scripts/init.d/helm-proof-checker_mowgli | 6 +++--- helm/scripts/init.d/helm-uri-set-queue | 5 +++-- helm/scripts/init.d/helm-uri-set-queue_mowgli | 7 ++++--- 6 files changed, 17 insertions(+), 13 deletions(-) diff --git a/helm/scripts/init.d/helm-draw-graph b/helm/scripts/init.d/helm-draw-graph index cdb5c0538..34490799e 100755 --- a/helm/scripts/init.d/helm-draw-graph +++ b/helm/scripts/init.d/helm-draw-graph @@ -6,7 +6,8 @@ # 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/draw_graph.cgi +DAEMON=/projects/helm/graphs/tools/drawGraph.opt USAGE="Usage: /etc/init.d/helm-draw-graph { start | stop | restart }" ENVSCRIPT="" diff --git a/helm/scripts/init.d/helm-draw-graph_mowgli b/helm/scripts/init.d/helm-draw-graph_mowgli index d1a08f9f6..769cd3f0d 100755 --- a/helm/scripts/init.d/helm-draw-graph_mowgli +++ b/helm/scripts/init.d/helm-draw-graph_mowgli @@ -6,7 +6,8 @@ # 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/draw_graph.cgi +DAEMON=/projects/helm/graphs/tools/drawGraph.opt USAGE="Usage: /etc/init.d/helm-draw-graph_mowgli { start | stop | restart }" ENVSCRIPT="" @@ -20,7 +21,7 @@ fi . $ENVSCRIPT &> /dev/null NAME=`basename $DAEMON` -PIDFILE=/projects/helm/run/$NAME.pid +PIDFILE=/projects/helm/run/"$NAME"_mowgli.pid do_start () { echo "Starting $DAEMON ..." diff --git a/helm/scripts/init.d/helm-proof-checker b/helm/scripts/init.d/helm-proof-checker index e96d10c4a..f3acbc12a 100755 --- a/helm/scripts/init.d/helm-proof-checker +++ b/helm/scripts/init.d/helm-proof-checker @@ -4,9 +4,9 @@ # # by --Zack # Created: Wed, 9 Oct 2002 11:12:01 +0200 -# Last-Modified: Wed, 9 Oct 2002 11:12:01 +0200 +# Last-Modified: Wed, 13 Nov 2002 18:30:09 +0100 -DAEMON=/projects/helm/proofChecker/proofChecker.pl +DAEMON=/projects/helm/proofChecker/proofChecker.opt USAGE="Usage: /etc/init.d/helm-proof-checker { start | stop | restart }" ENVSCRIPT="" diff --git a/helm/scripts/init.d/helm-proof-checker_mowgli b/helm/scripts/init.d/helm-proof-checker_mowgli index 97874eb1e..fac648138 100755 --- a/helm/scripts/init.d/helm-proof-checker_mowgli +++ b/helm/scripts/init.d/helm-proof-checker_mowgli @@ -4,9 +4,9 @@ # # by --Zack # Created: Wed, 9 Oct 2002 11:12:01 +0200 -# Last-Modified: Wed, 9 Oct 2002 11:12:01 +0200 +# Last-Modified: Wed, 13 Nov 2002 18:30:39 +0100 -DAEMON=/projects/helm/proofChecker_mowgli/proofChecker.pl +DAEMON=/projects/helm/proofChecker_mowgli/proofChecker.opt USAGE="Usage: /etc/init.d/helm-proof-checker { start | stop | restart }" ENVSCRIPT="" @@ -20,7 +20,7 @@ fi . $ENVSCRIPT &> /dev/null NAME=`basename $DAEMON` -PIDFILE=/projects/helm/run/$NAME.pid +PIDFILE=/projects/helm/run/"$NAME"_mowgli.pid do_start () { echo "Starting $DAEMON ..." diff --git a/helm/scripts/init.d/helm-uri-set-queue b/helm/scripts/init.d/helm-uri-set-queue index 771140539..242545a7b 100755 --- a/helm/scripts/init.d/helm-uri-set-queue +++ b/helm/scripts/init.d/helm-uri-set-queue @@ -4,9 +4,10 @@ # # by --Zack # Created: Tue, 8 Oct 2002 17:18:17 +0200 -# Last-Modified: Wed, 9 Oct 2002 11:12:01 +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/uri_set_queue.cgi +DAEMON=/projects/helm/graphs/tools/uriSetQueue.opt USAGE="Usage: /etc/init.d/helm-uri-set-queue { start | stop | restart }" ENVSCRIPT="" diff --git a/helm/scripts/init.d/helm-uri-set-queue_mowgli b/helm/scripts/init.d/helm-uri-set-queue_mowgli index 36c195e1d..2a0388068 100755 --- a/helm/scripts/init.d/helm-uri-set-queue_mowgli +++ b/helm/scripts/init.d/helm-uri-set-queue_mowgli @@ -4,9 +4,10 @@ # # by --Zack # Created: Tue, 8 Oct 2002 17:18:17 +0200 -# Last-Modified: Wed, 9 Oct 2002 11:12:01 +0200 +# Last-Modified: Wed, 20 Nov 2002 10:50:25 +0100 -DAEMON=/projects/helm/graphs/tools/uri_set_queue.cgi +#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_mowgli { start | stop | restart }" ENVSCRIPT="" @@ -20,7 +21,7 @@ fi . $ENVSCRIPT &> /dev/null NAME=`basename $DAEMON` -PIDFILE=/projects/helm/run/$NAME.pid +PIDFILE=/projects/helm/run/"$NAME"_mowgli.pid do_start () { echo "Starting $DAEMON ..." -- 2.39.2