# HG changeset patch
# User wenzelm
# Date 1004113005 -7200
# Node ID 38e20c036e375e7f81b90b1fb1d037c83489d7da
# Parent  9c812b21b2e842c8213fb32f786f436fcd754517
tuned;

diff -r 9c812b21b2e8 -r 38e20c036e37 lib/Tools/usedir
--- a/lib/Tools/usedir	Fri Oct 26 18:16:31 2001 +0200
+++ b/lib/Tools/usedir	Fri Oct 26 18:16:45 2001 +0200
@@ -168,7 +168,9 @@
 
 PARENT=$(basename "$LOGIC")
 
-[ -z "$BUILD" ] && cd "$NAME"
+if [ -z "$BUILD" ]; then
+  cd "$NAME" || fail "Bad session directory '$NAME'"
+fi
 
 if [ "$DOCUMENT" != false ]; then
   DOC="$DOCUMENT"