lib/scripts/getsettings
changeset 73523 2cd23d587db9
parent 73520 4cba4e250c28
child 73988 678e1c9eb009
equal deleted inserted replaced
73522:b219774a71ae 73523:2cd23d587db9
    69 if [ -z "$ISABELLE_PLATFORM_FAMILY" ]; then
    69 if [ -z "$ISABELLE_PLATFORM_FAMILY" ]; then
    70   echo 1>&2 "Failed to determine hardware and operating system type!"
    70   echo 1>&2 "Failed to determine hardware and operating system type!"
    71   exit 2
    71   exit 2
    72 fi
    72 fi
    73 
    73 
    74 #Isabelle distribution identifier -- filled in automatically!
    74 if [ -z "$ISABELLE_IDENTIFIER" -a -f "$ISABELLE_HOME/etc/ISABELLE_IDENTIFIER" ]
    75 [ -z "$ISABELLE_IDENTIFIER" ] && ISABELLE_IDENTIFIER=""
    75 then
       
    76   ISABELLE_IDENTIFIER="$(cat "$ISABELLE_HOME/etc/ISABELLE_IDENTIFIER")"
       
    77 fi
       
    78 
       
    79 ISABELLE_NAME="${ISABELLE_IDENTIFIER:-Isabelle}"
    76 
    80 
    77 
    81 
    78 # components
    82 # components
    79 
    83 
    80 ISABELLE_COMPONENTS=""
    84 ISABELLE_COMPONENTS=""