# HG changeset patch
# User wenzelm
# Date 1114537779 -7200
# Node ID d5bd4a18ce709a84e6de8656d14a480fae6d8c84
# Parent  30a4267c6301816f0b5db399ee027398d124fa1d
improved handling of symlinks;

diff -r 30a4267c6301 -r d5bd4a18ce70 bin/isabelle
--- a/bin/isabelle	Tue Apr 26 17:44:24 2005 +0200
+++ b/bin/isabelle	Tue Apr 26 19:49:39 2005 +0200
@@ -5,11 +5,12 @@
 #
 # Smart selection of isabelle-process versus isabelle-interface.
 
-THIS="$0"
-while [ -L "$THIS" ]; do
-    THIS="$(dirname "$THIS")/$(LC_ALL=C ls -l "$THIS" | sed 's/.* -> //')"
-done
-THIS="$(cd "$(dirname "$THIS")"; pwd)"
+if [ -L "$0" ]; then
+  TARGET="$(LC_ALL=C ls -l "$0" | sed 's/.* -> //')"
+  exec $(cd "$(dirname "$0")"; cd "$(dirname "$TARGET")"; pwd)/$(basename "$TARGET") "$@"
+fi
+
+THIS=$(cd "$(dirname "$0")"; pwd)
 NAME="$(basename "$0")"
 
 case "$NAME" in
diff -r 30a4267c6301 -r d5bd4a18ce70 bin/isabelle-interface
--- a/bin/isabelle-interface	Tue Apr 26 17:44:24 2005 +0200
+++ b/bin/isabelle-interface	Tue Apr 26 19:49:39 2005 +0200
@@ -5,16 +5,17 @@
 #
 # Isabelle interface startup script.
 
+if [ -L "$0" ]; then
+  TARGET="$(LC_ALL=C ls -l "$0" | sed 's/.* -> //')"
+  exec $(cd "$(dirname "$0")"; cd "$(dirname "$TARGET")"; pwd)/$(basename "$TARGET") "$@"
+fi
+
 
 ## settings
 
 PRG="$(basename "$0")"
 
-THIS="$0"
-while [ -L "$THIS" ]; do
-    THIS="$(dirname "$THIS")/$(LC_ALL=C ls -l "$THIS" | sed 's/.* -> //')"
-done
-ISABELLE_HOME="$(cd "$(dirname "$THIS")/.."; pwd)"
+ISABELLE_HOME="$(dirname "$0")/.."
 . "$ISABELLE_HOME/lib/scripts/getsettings" || \
   { echo "$PRG probably not called from its original place!"; exit 2; }
 
diff -r 30a4267c6301 -r d5bd4a18ce70 bin/isabelle-process
--- a/bin/isabelle-process	Tue Apr 26 17:44:24 2005 +0200
+++ b/bin/isabelle-process	Tue Apr 26 19:49:39 2005 +0200
@@ -5,16 +5,17 @@
 #
 # Isabelle process startup script.
 
+if [ -L "$0" ]; then
+  TARGET="$(LC_ALL=C ls -l "$0" | sed 's/.* -> //')"
+  exec $(cd "$(dirname "$0")"; cd "$(dirname "$TARGET")"; pwd)/$(basename "$TARGET") "$@"
+fi
+
 
 ## settings
 
 PRG="$(basename "$0")"
 
-THIS="$0"
-while [ -L "$THIS" ]; do
-    THIS="$(dirname "$THIS")/$(LC_ALL=C ls -l "$THIS" | sed 's/.* -> //')"
-done
-ISABELLE_HOME="$(cd "$(dirname "$THIS")/.."; pwd)"
+ISABELLE_HOME="$(dirname "$0")/.."
 . "$ISABELLE_HOME/lib/scripts/getsettings" || \
   { echo "$PRG probably not called from its original place!"; exit 2; }
 
diff -r 30a4267c6301 -r d5bd4a18ce70 bin/isatool
--- a/bin/isatool	Tue Apr 26 17:44:24 2005 +0200
+++ b/bin/isatool	Tue Apr 26 19:49:39 2005 +0200
@@ -6,6 +6,11 @@
 # Isabelle tool starter -- provides settings environment
 # and keeps your PATH name space clean.
 
+if [ -L "$0" ]; then
+  TARGET="$(LC_ALL=C ls -l "$0" | sed 's/.* -> //')"
+  exec $(cd "$(dirname "$0")"; cd "$(dirname "$TARGET")"; pwd)/$(basename "$TARGET") "$@"
+fi
+
 
 ## settings