- script.sh added to the repository: you should change it to reflect your

[helm.git] / helm / gTopLevel / script.sh

diff --git a/helm/gTopLevel/script.sh b/helm/gTopLevel/script.sh
new file mode 100755 (executable)
index 0000000..29dd0a3
--- /dev/null
+++ b/helm/gTopLevel/script.sh
@@ -0,0 +1,19 @@
+#!/bin/bash
+
+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_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 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