bin/isabelle
changeset 15784 3a214de33d53
parent 15778 98af3693f6b3
child 15843 d5bd4a18ce70
equal deleted inserted replaced
15783:82e40c9a0f3f 15784:3a214de33d53
     7 
     7 
     8 THIS="$0"
     8 THIS="$0"
     9 while [ -L "$THIS" ]; do
     9 while [ -L "$THIS" ]; do
    10     THIS="$(dirname "$THIS")/$(LC_ALL=C ls -l "$THIS" | sed 's/.* -> //')"
    10     THIS="$(dirname "$THIS")/$(LC_ALL=C ls -l "$THIS" | sed 's/.* -> //')"
    11 done
    11 done
    12 THIS="$(cd "$(dirname "$(readlink -f "$THIS")")"; pwd)"
    12 THIS="$(cd "$(dirname "$THIS")"; pwd)"
    13 NAME="$(basename "$0")"
    13 NAME="$(basename "$0")"
    14 
    14 
    15 case "$NAME" in
    15 case "$NAME" in
    16   I*)
    16   I*)
    17     PRG=isabelle-interface
    17     PRG=isabelle-interface