lib/scripts/getsettings
changeset 28055 eb855c3db657
parent 27940 002718f9c938
child 28499 eff93bc3c14f
equal deleted inserted replaced
28054:2b84d34c5d02 28055:eb855c3db657
    51   ISABELLE_ROOT_JVM="$(jvmpath /)"
    51   ISABELLE_ROOT_JVM="$(jvmpath /)"
    52 else
    52 else
    53   function jvmpath() { echo "$@"; }
    53   function jvmpath() { echo "$@"; }
    54   ISABELLE_ROOT_JVM=/
    54   ISABELLE_ROOT_JVM=/
    55 fi
    55 fi
       
    56 HOME_JVM="$HOME"
    56 
    57 
    57 #CLASSPATH convenience
    58 #CLASSPATH convenience
    58 function classpath () {
    59 function classpath () {
    59   for X in "$@"
    60   for X in "$@"
    60   do
    61   do