From: Stefano Zacchiroli Date: Tue, 16 Dec 2003 13:50:41 +0000 (+0000) Subject: sample script.sh which read META files from ocaml/METAS X-Git-Tag: V_0_2_2~11 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=55f687f3e960c10d77c88993b142d712ebd46836;p=helm.git sample script.sh which read META files from ocaml/METAS --- diff --git a/helm/gTopLevel/script.sh b/helm/gTopLevel/script.sh index 6be688132..5592e25d8 100755 --- a/helm/gTopLevel/script.sh +++ b/helm/gTopLevel/script.sh @@ -1,22 +1,17 @@ -#!/bin/bash +export OCAMLPATH="/home/zack/dati/HELM/galax:/home/zack/dati/HELM/cvs/helm/ocaml/METAS:/home/zack/dati/HELM/cvs/helm:/home/zack/helm/hbugs/meta" -#export OCAMLPATH=/projects/helm/galax/sources/natile-galax-0.1-alpha-installed/lib:/home/luca/miohelm/helm/ocaml:/home/luca/miohelm/helm:/home/luca/miohelm/helm/hbugs/meta:/home/luca/miohelm/helm/gTopLevel - -export OCAMLPATH=/home/asperti/helm/ocaml:/home/asperti/helm/hbugs/meta:/local/helm/galax/sources/natile-galax-0.1-alpha-installed/lib - -export HELM_ANNOTATIONS_DIR=/home/luca/miohelm/objects -export HELM_ANNOTATIONS_URL=file:///home/luca/miohelm/objects +export HELM_ANNOTATIONS_DIR=/home/zack/miohelm/objects +export HELM_ANNOTATIONS_URL=file:///home/zack/miohelm/objects export HELM_GETTER_URL=http://localhost:58081/ -export HELM_PROCESSOR_URL=http://localhost:8080/helm/servlet/uwobo/ -#export HELM_GETTER_URL=http://mowgli.cs.unibo.it:58081/ -#export HELM_PROCESSOR_URL=http://mowgli.cs.unibo.it:8081/mowgli/servlet/uwobo/ +export HELM_PROCESSOR_URL=http://localhost:58080/ -export HELM_TMP_DIR=/tmp +export GTOPLEVEL_PROOFFILE=/public/helm_library/currentproof +export GTOPLEVEL_PROOFFILETYPE=/public/helm_library/currentprooftype +export GTOPLEVEL_INNERTYPESFILE=/public/helm_library/innertypes +export GTOPLEVEL_CONSTANTTYPEFILE=/public/helm_library/constanttype +export GTOPLEVEL_ENVIRONMENTFILE=/public/helm_library/environment +export MATHQL_DB_MAP=/home/zack/helm/mathql_db_map.txt +export POSTGRESQL_CONNECTION_STRING="dbname=mowgli" -export GTOPLEVEL_PROOFFILE=/tmp/asperti_currentproof -export GTOPLEVEL_PROOFFILETYPE=/tmp/asperti_currentprooftype -export GTOPLEVEL_INNERTYPESFILE=/tmp/asperti_innertypes -export GTOPLEVEL_CONSTANTTYPEFILE=/tmp/asperti_constanttype -export POSTGRESQL_CONNECTION_STRING="host=mowgli.cs.unibo.it dbname=mowgli user=helm password=awH21Un" -#export POSTGRESQL_CONNECTION_STRING="dbname=helm_mowgli_new_schema user=helm" -#export POSTGRESQL_CONNECTION_STRING="host=mowgli.cs.unibo.it dbname=helm_mowgli_new_schema user=helm" +export HELM_TMP_DIR=/tmp +unset http_proxy