]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/gTopLevel/script.sh
removed dependency on netclient, use http_client module from ocaml-http
[helm.git] / helm / gTopLevel / script.sh
index 29dd0a396dce1de19d582218102119d205c1e1ce..5592e25d856058ff39d47027fec9e0cfdffdf8dd 100755 (executable)
@@ -1,19 +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/claudio/miohelm/helm/ocaml:/home/claudio/miohelm/helm:/home/claudio/miohelm/helm/hbugs/meta
-
-export HELM_ANNOTATIONS_DIR=/home/claudio/miohelm/objects
-export HELM_ANNOTATIONS_URL=file:///home/claudio/miohelm/objects
-#export HELM_GETTER_URL=http://mowgli.cs.unibo.it:58081/
-#export HELM_PROCESSOR_URL=http://mowgli.cs.unibo.it:58080/
+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:58080/
 
-export GTOPLEVEL_PROOFFILE=/public/sacerdot/currentproof
-export GTOPLEVEL_PROOFFILETYPE=/public/sacerdot/currentprooftype
-export GTOPLEVEL_INNERTYPESFILE=/public/sacerdot/innertypes
-export GTOPLEVEL_CONSTANTTYPEFILE=/public/sacerdot/constanttype
+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 POSTGRESQL_CONNECTION_STRING="host=mowgli.cs.unibo.it dbname=mowgli user=helm password=awH21Un"
 
 export HELM_TMP_DIR=/tmp
+unset http_proxy