# HG changeset patch
# User wenzelm
# Date 1378495687 -7200
# Node ID 4adb2cce5fc64da1fb7472df1e9a3b5af0b79b63
# Parent  811db2b751ed9ba9da1d325c5d4dba2ce1105ca1
use JEDIT_OPTIONS only once (in isabelle.Main.start_jedit);

diff -r 811db2b751ed -r 4adb2cce5fc6 src/Tools/jEdit/lib/Tools/jedit
--- a/src/Tools/jEdit/lib/Tools/jedit	Fri Sep 06 21:13:19 2013 +0200
+++ b/src/Tools/jEdit/lib/Tools/jedit	Fri Sep 06 21:28:07 2013 +0200
@@ -171,7 +171,7 @@
 
 declare -a JAVA_ARGS; eval "JAVA_ARGS=($JEDIT_JAVA_OPTIONS $JEDIT_SYSTEM_OPTIONS)"
 
-declare -a ARGS; eval "ARGS=($JEDIT_OPTIONS)"
+declare -a ARGS=()
 
 declare -a OPTIONS; eval "OPTIONS=($ISABELLE_JEDIT_OPTIONS)"
 getoptions "${OPTIONS[@]}"