From: Claudio Sacerdoti Coen Date: Mon, 19 Jan 2004 17:41:47 +0000 (+0000) Subject: Scripts simplified (since now we have only one cluster and only one X-Git-Tag: V_0_5_1_3~16 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=8f2461e7c0c1a6b7d54c16e84b49b2773ea4788d;p=helm.git Scripts simplified (since now we have only one cluster and only one stable version of the library). --- diff --git a/helm/scripts/Makefile b/helm/scripts/Makefile index 8b20831af..be6ba2198 100644 --- a/helm/scripts/Makefile +++ b/helm/scripts/Makefile @@ -1,19 +1,15 @@ all: - - chmod ug+w marcello*rc phd*rc - ./makeit V7_mowgli marcello marcello marcello_mowgli.cshrc - ./makeit V7_mowgli marcello marcello marcello_mowgli.rc - ./makeit V7_mowgli marcello phd marcello_phd_mowgli.cshrc - ./makeit V7_mowgli marcello phd marcello_phd_mowgli.rc - ./makeit V7_mowgli phd phd phd_mowgli.cshrc - ./makeit V7_mowgli phd phd phd_mowgli.rc - ./makeit V7_mowgli phd marcello phd_marcello_mowgli.cshrc - ./makeit V7_mowgli phd marcello phd_marcello_mowgli.rc - chmod a+x marcello*rc phd*rc - chmod ug-w marcello*rc phd*rc + - chmod ug+w phd*rc + ./makeit phd phd_mowgli.cshrc + ./makeit phd phd_mowgli.rc + ./makeit marcello phd_marcello_mowgli.cshrc + ./makeit marcello phd_marcello_mowgli.rc + chmod a+x phd*rc + chmod ug-w phd*rc clean: - rm -f marcello*rc phd*rc + rm -f phd*rc cleanbak: rm -f *~ diff --git a/helm/scripts/makeit b/helm/scripts/makeit index afad01f3c..64553523e 100755 --- a/helm/scripts/makeit +++ b/helm/scripts/makeit @@ -1,11 +1,10 @@ #!/bin/sh -if test $# != 3; then - echo "Usage: makeit " +if test $# != 1; then + echo "Usage: makeit " echo - echo " must be V7_mowgli" - echo " is either phd or marcello" + echo " is the machine we connect from" exit 1 fi -sed -e "s/@COQV@/$1/" -e "s/@WHERE@/$2/" -e "s/@FROM@/$3/" +sed -e "s/@FROM@/$1/" diff --git a/helm/scripts/template.cshrc b/helm/scripts/template.cshrc index 1038c90d9..7cba3740b 100644 --- a/helm/scripts/template.cshrc +++ b/helm/scripts/template.cshrc @@ -1,31 +1,13 @@ -set COQV=@COQV@ -set WHERE=@WHERE@ +set COQV=V7_mowgli +set WHERE=phd set FROM=@FROM@ setenv CVS_RSH=ssh echo "Configuring HELM for $WHERE (from $FROM), Coq $COQV" -if ($WHERE == phd) then - setenv HELMROOT /projects/helm - setenv JAVA_HOME /opt/java/jdk1.3 - setenv PATH .:$JAVA_HOME/bin/:$PATH - if ($?LD_LIBRARY_PATH == 1) then - setenv LD_LIBRARY_PATH /usr/local/lib:$LD_LIBRARY_PATH - else - setenv LD_LIBRARY_PATH /usr/local/lib - endif -else - setenv HELMROOT /home/projects/helm - setenv JAVA_HOME /usr/local/jdk1.3 - setenv PATH .:$JAVA_HOME/bin:$HELMROOT/local/bin:$PATH - if ($?LD_LIBRARY_PATH == 1) then - setenv LD_LIBRARY_PATH $HELMROOT/local/lib:$LD_LIBRARY_PATH - else - setenv LD_LIBRARY_PATH $HELMROOT/local/lib - endif -endif +setenv HELMROOT /projects/helm if ($WHERE == $FROM) then set FONTROOT=$HELMROOT @@ -52,20 +34,16 @@ setenv HTTP_GETTER_XSLT_INDEXNAME xslt_index.txt setenv HELM_ANNOTATIONS_DIR pippo setenv HELM_ANNOTATIONS_URL pippo setenv UWOBO_PANEL_CONF /projects/helm/public_html/uwobo/panel/control.html -if ($COQV == V7_mowgli) then - setenv UWOBO_PORT 58080 - setenv UWOBO_LOG_FILE /projects/helm/log/uwobo - setenv HTTP_GETTER_PORT 58081 - setenv URI_SET_QUEUE_PORT 58082 - setenv DRAW_GRAPH_PORT 58083 - setenv PROOF_CHECKER_PORT 58084 - setenv SEARCH_ENGINE_PORT 58085 - setenv DRAW_GRAPH_DIR /projects/helm/daemons/graphs/tools - setenv HELM_UWOBO_URL http://mowgli.cs.unibo.it:$UWOBO_PORT/ - setenv HTTP_GETTER_DTD_BASE_URL http://mowgli.cs.unibo.it/dtd -else - echo "Error: Version $COQV not recognized" -endif +setenv UWOBO_PORT 58080 +setenv UWOBO_LOG_FILE /projects/helm/log/uwobo +setenv HTTP_GETTER_PORT 58081 +setenv URI_SET_QUEUE_PORT 58082 +setenv DRAW_GRAPH_PORT 58083 +setenv PROOF_CHECKER_PORT 58084 +setenv SEARCH_ENGINE_PORT 58085 +setenv DRAW_GRAPH_DIR /projects/helm/daemons/graphs/tools +setenv HELM_UWOBO_URL http://mowgli.cs.unibo.it:$UWOBO_PORT/ +setenv HTTP_GETTER_DTD_BASE_URL http://mowgli.cs.unibo.it/dtd setenv HELM_GETTER_URL http://mowgli.cs.unibo.it:$HTTP_GETTER_PORT/ setenv SEARCH_ENGINE_HTML_DIR /projects/helm/daemon/searchEngine/html diff --git a/helm/scripts/template.rc b/helm/scripts/template.rc index 629ce1c22..c22271bcf 100644 --- a/helm/scripts/template.rc +++ b/helm/scripts/template.rc @@ -1,23 +1,13 @@ -COQV=@COQV@ -WHERE=@WHERE@ +COQV=V7_mowgli +WHERE=phd FROM=@FROM@ export CVS_RSH=ssh echo "Configuring HELM for $WHERE (from $FROM), Coq $COQV" -if test $WHERE = phd; then - export HELMROOT=/projects/helm - export JAVA_HOME=/opt/java/jdk1.3 - export PATH=.:$JAVA_HOME/bin/:$PATH - export LD_LIBRARY_PATH=/usr/local/lib:$LD_LIBRARY_PATH -else - export HELMROOT=/home/projects/helm - export JAVA_HOME=/usr/local/jdk1.3 - export PATH=.:$JAVA_HOME/bin:$HELMROOT/local/bin:$PATH - export LD_LIBRARY_PATH=$HELMROOT/local/lib:$LD_LIBRARY_PATH -fi +export HELMROOT=/projects/helm if test $WHERE = $FROM; then FONTROOT=$HELMROOT @@ -44,20 +34,16 @@ export HTTP_GETTER_XSLT_INDEXNAME=xslt_index.txt export HELM_ANNOTATIONS_DIR=pippo export HELM_ANNOTATIONS_URL=pippo export UWOBO_PANEL_CONF=/projects/helm/public_html/uwobo/panel/control.html -if test $COQV = V7_mowgli; then - export UWOBO_PORT=58080 - export UWOBO_LOG_FILE=/projects/helm/log/uwobo - export HTTP_GETTER_PORT=58081 - export URI_SET_QUEUE_PORT=58082 - export DRAW_GRAPH_PORT=58083 - export PROOF_CHECKER_PORT=58084 - export SEARCH_ENGINE_PORT=58085 - export DRAW_GRAPH_DIR=/projects/helm/daemons/graphs/tools - export HELM_UWOBO_URL=http://mowgli.cs.unibo.it:$UWOBO_PORT/ - export HTTP_GETTER_DTD_BASE_URL=http://mowgli.cs.unibo.it/dtd -else - echo "Error: Version $COQV not recognized" -fi +export UWOBO_PORT=58080 +export UWOBO_LOG_FILE=/projects/helm/log/uwobo +export HTTP_GETTER_PORT=58081 +export URI_SET_QUEUE_PORT=58082 +export DRAW_GRAPH_PORT=58083 +export PROOF_CHECKER_PORT=58084 +export SEARCH_ENGINE_PORT=58085 +export DRAW_GRAPH_DIR=/projects/helm/daemons/graphs/tools +export HELM_UWOBO_URL=http://mowgli.cs.unibo.it:$UWOBO_PORT/ +export HTTP_GETTER_DTD_BASE_URL=http://mowgli.cs.unibo.it/dtd export HELM_GETTER_URL=http://mowgli.cs.unibo.it:$HTTP_GETTER_PORT/ export SEARCH_ENGINE_HTML_DIR=/projects/helm/daemons/searchEngine/html