use JEDIT_OPTIONS only once (in isabelle.Main.start_jedit);
authorwenzelm
Fri, 06 Sep 2013 21:28:07 +0200
changeset 53446 4adb2cce5fc6
parent 53445 811db2b751ed
child 53447 3d8dfddefe84
use JEDIT_OPTIONS only once (in isabelle.Main.start_jedit);
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[@]}"