bin/isabelle-process
changeset 15967 f9163c6f69d6
parent 15864 cc1b4a289321
child 16101 37471d84d353
equal deleted inserted replaced
15966:73cf5ef8ed20 15967:f9163c6f69d6
     5 #
     5 #
     6 # Isabelle process startup script.
     6 # Isabelle process startup script.
     7 
     7 
     8 if [ -L "$0" ]; then
     8 if [ -L "$0" ]; then
     9   TARGET="$(LC_ALL=C ls -l "$0" | sed 's/.* -> //')"
     9   TARGET="$(LC_ALL=C ls -l "$0" | sed 's/.* -> //')"
    10   exec "$(cd "$(dirname "$0")"; cd "$(dirname "$TARGET")"; pwd)/$(basename "$TARGET")" "$@"
    10   exec "$(cd "$(dirname "$0")"; cd "$(pwd -P)"; cd "$(dirname "$TARGET")"; pwd)/$(basename "$TARGET")" "$@"
    11 fi
    11 fi
    12 
    12 
    13 
    13 
    14 ## settings
    14 ## settings
    15 
    15 
    16 PRG="$(basename "$0")"
    16 PRG="$(basename "$0")"
    17 
    17 
    18 ISABELLE_HOME="$(dirname "$0")/.."
    18 ISABELLE_HOME="$(cd "$(dirname "$0")"; cd "$(pwd -P)"; cd ..; pwd)"
    19 . "$ISABELLE_HOME/lib/scripts/getsettings" || \
    19 source "$ISABELLE_HOME/lib/scripts/getsettings" || exit 2
    20   { echo "$PRG probably not called from its original place!"; exit 2; }
       
    21 
    20 
    22 
    21 
    23 ## diagnostics
    22 ## diagnostics
    24 
    23 
    25 function usage()
    24 function usage()