Index: tools/Scripts/Logon
===================================================================
--- tools/Scripts/Logon	(revision 194)
+++ tools/Scripts/Logon	(revision 195)
@@ -3,5 +3,5 @@
 # This script should be sourced at log on (e.g. in .bashrc)
 
-export REPOS_DIR=$(cd "${0%/*}/../.." 2>/dev/null; echo "$PWD")
+export REPOS_DIR=$1
 if [ -z "$DIM_DNS_NODE" ]; then export DIM_DNS_NODE=ihp-pc1.ethz.ch; fi
 export DIM_HOST_NODE=$HOST.ethz.ch