Allow symlinks to shell scripts
authorgagern
Wed, 20 Apr 2005 14:18:33 +0200
changeset 15778 98af3693f6b3
parent 15777 311aedc96e71
child 15779 aed221aff642
Allow symlinks to shell scripts
NEWS
bin/isabelle
bin/isabelle-interface
bin/isabelle-process
--- a/NEWS	Wed Apr 20 00:45:54 2005 +0200
+++ b/NEWS	Wed Apr 20 14:18:33 2005 +0200
@@ -344,6 +344,9 @@
 * isatool usedir: option -f allows specification of the ML file to be
   used by Isabelle; default is ROOT.ML.
 
+* symlinks to Isabelle, isabelle, isabelle-interface and isabelle-process
+  are allowed; isabelle directories are determined based on link target.
+
 * ISABELLE_DOC_FORMAT setting specifies preferred document format (for
   isatool doc, isatool mkdir, display_drafts etc.).
 
--- a/bin/isabelle	Wed Apr 20 00:45:54 2005 +0200
+++ b/bin/isabelle	Wed Apr 20 14:18:33 2005 +0200
@@ -5,7 +5,11 @@
 #
 # Smart selection of isabelle-process versus isabelle-interface.
 
-THIS=$(cd "$(dirname "$0")"; pwd)
+THIS="$0"
+while [ -L "$THIS" ]; do
+    THIS="$(dirname "$THIS")/$(LC_ALL=C ls -l "$THIS" | sed 's/.* -> //')"
+done
+THIS="$(cd "$(dirname "$(readlink -f "$THIS")")"; pwd)"
 NAME="$(basename "$0")"
 
 case "$NAME" in
--- a/bin/isabelle-interface	Wed Apr 20 00:45:54 2005 +0200
+++ b/bin/isabelle-interface	Wed Apr 20 14:18:33 2005 +0200
@@ -10,7 +10,11 @@
 
 PRG="$(basename "$0")"
 
-ISABELLE_HOME="$(dirname "$0")/.."
+THIS="$0"
+while [ -L "$THIS" ]; do
+    THIS="$(dirname "$THIS")/$(LC_ALL=C ls -l "$THIS" | sed 's/.* -> //')"
+done
+ISABELLE_HOME="$(cd "$(dirname "$(readlink -f "$THIS")")/.."; pwd)"
 . "$ISABELLE_HOME/lib/scripts/getsettings" || \
   { echo "$PRG probably not called from its original place!"; exit 2; }
 
--- a/bin/isabelle-process	Wed Apr 20 00:45:54 2005 +0200
+++ b/bin/isabelle-process	Wed Apr 20 14:18:33 2005 +0200
@@ -10,7 +10,11 @@
 
 PRG="$(basename "$0")"
 
-ISABELLE_HOME="$(dirname "$0")/.."
+THIS="$0"
+while [ -L "$THIS" ]; do
+    THIS="$(dirname "$THIS")/$(LC_ALL=C ls -l "$THIS" | sed 's/.* -> //')"
+done
+ISABELLE_HOME="$(cd "$(dirname "$(readlink -f "$THIS")")/.."; pwd)"
 . "$ISABELLE_HOME/lib/scripts/getsettings" || \
   { echo "$PRG probably not called from its original place!"; exit 2; }