1.1 --- a/src/Tools/jEdit/dist-template/interface	Thu Aug 13 16:01:55 2009 +0200
     1.2 +++ b/src/Tools/jEdit/dist-template/interface	Sat Aug 22 22:54:36 2009 +0200
     1.3 @@ -44,10 +44,10 @@
     1.4  do
     1.5    case "$OPT" in
     1.6      J)
     1.7 -      JAVA_OPTIONS+=("$OPTARG")
     1.8 +      JAVA_OPTIONS["${#JAVA_OPTIONS[@]}"]="$OPTARG"
     1.9        ;;
    1.10      j)
    1.11 -      OPTIONS+=("$OPTARG")
    1.12 +      OPTIONS["${#OPTIONS[@]}"]="$OPTARG"
    1.13        ;;
    1.14      l)
    1.15        JEDIT_LOGIC="$OPTARG"
    1.16 @@ -73,10 +73,10 @@
    1.17  declare -a FILES=()
    1.18  
    1.19  if [ "$#" -eq 0 ]; then
    1.20 -  FILES+=(Scratch.thy)
    1.21 +  FILES["${#FILES[@]}"]="Scratch.thy"
    1.22  else
    1.23    while [ "$#" -gt 0 ]; do
    1.24 -    FILES+=($(jvmpath "$1"))
    1.25 +    FILES["${#FILES[@]}"]="$(jvmpath "$1")"
    1.26      shift
    1.27    done
    1.28  fi