- script.sh removed from CVS. script.sh.sample added isntead

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

diff --git a/helm/gTopLevel/script.sh b/helm/gTopLevel/script.sh
deleted file mode 100755 (executable)
index 848103c..0000000
--- a/helm/gTopLevel/script.sh
+++ /dev/null
@@ -1,16 +0,0 @@
-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 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/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 HELM_TMP_DIR=/tmp
-unset http_proxy