less ambitious array operations -- for improved compatibility with older versions of bash;

--- a/src/Tools/jEdit/dist-template/interface	Thu Aug 13 16:01:55 2009 +0200
+++ b/src/Tools/jEdit/dist-template/interface	Sat Aug 22 22:54:36 2009 +0200
@@ -44,10 +44,10 @@
 do
   case "$OPT" in
     J)
-      JAVA_OPTIONS+=("$OPTARG")
+      JAVA_OPTIONS["${#JAVA_OPTIONS[@]}"]="$OPTARG"
       ;;
     j)
-      OPTIONS+=("$OPTARG")
+      OPTIONS["${#OPTIONS[@]}"]="$OPTARG"
       ;;
     l)
       JEDIT_LOGIC="$OPTARG"
@@ -73,10 +73,10 @@
 declare -a FILES=()
 
 if [ "$#" -eq 0 ]; then
-  FILES+=(Scratch.thy)
+  FILES["${#FILES[@]}"]="Scratch.thy"
 else
   while [ "$#" -gt 0 ]; do
-    FILES+=($(jvmpath "$1"))
+    FILES["${#FILES[@]}"]="$(jvmpath "$1")"
     shift
   done
 fi