bin/isabelle-process
changeset 15784 3a214de33d53
parent 15779 aed221aff642
child 15801 d2f5ca3c048d
equal deleted inserted replaced
15783:82e40c9a0f3f 15784:3a214de33d53
    15 
    15 
    16 THIS="$0"
    16 THIS="$0"
    17 while [ -L "$THIS" ]; do
    17 while [ -L "$THIS" ]; do
    18     THIS="$(dirname "$THIS")/$(LC_ALL=C ls -l "$THIS" | sed 's/.* -> //')"
    18     THIS="$(dirname "$THIS")/$(LC_ALL=C ls -l "$THIS" | sed 's/.* -> //')"
    19 done
    19 done
    20 ISABELLE_HOME="$(cd "$(dirname "$(readlink -f "$THIS")")/.."; pwd)"
    20 ISABELLE_HOME="$(cd "$(dirname "$THIS")/.."; pwd)"
    21 . "$ISABELLE_HOME/lib/scripts/getsettings" || \
    21 . "$ISABELLE_HOME/lib/scripts/getsettings" || \
    22   { echo "$PRG probably not called from its original place!"; exit 2; }
    22   { echo "$PRG probably not called from its original place!"; exit 2; }
    23 
    23 
    24 
    24 
    25 ## diagnostics
    25 ## diagnostics