src/Tools/jEdit/dist-template/lib/Tools/jedit
changeset 34843 eb8806a2e348
parent 34790 643c48774b17
child 34880 f88fc4fcab86
equal deleted inserted replaced
34842:2f6f9b6099b2 34843:eb8806a2e348
    75     esac
    75     esac
    76   done
    76   done
    77 }
    77 }
    78 
    78 
    79 declare -a JAVA_ARGS; eval "JAVA_ARGS=($JEDIT_JAVA_OPTIONS)"
    79 declare -a JAVA_ARGS; eval "JAVA_ARGS=($JEDIT_JAVA_OPTIONS)"
       
    80 [ -n "$SCALA_HOME" ] && JAVA_ARGS["${#JAVA_ARGS[@]}"]="-Dscala.home=$SCALA_HOME"
       
    81 
    80 declare -a ARGS; eval "ARGS=($JEDIT_OPTIONS)"
    82 declare -a ARGS; eval "ARGS=($JEDIT_OPTIONS)"
    81 
    83 
    82 declare -a OPTIONS; eval "OPTIONS=($ISABELLE_JEDIT_OPTIONS)"
    84 declare -a OPTIONS; eval "OPTIONS=($ISABELLE_JEDIT_OPTIONS)"
    83 getoptions "${OPTIONS[@]}"
    85 getoptions "${OPTIONS[@]}"
    84 
    86