# HG changeset patch
# User wenzelm
# Date 1250974476 -7200
# Node ID 73d53ad05b144ba7120195c2d2692b8b4cc3a4bd
# Parent  ab54955c9eeab4cb0b68b0561d05e065f8c77a0b
less ambitious array operations -- for improved compatibility with older versions of bash;

diff -r ab54955c9eea -r 73d53ad05b14 src/Tools/jEdit/dist-template/interface
--- 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