Mon, 09 Sep 2013 13:48:06 +0200 generate application based on $JEDIT_JAVA_OPTIONS $JEDIT_SYSTEM_OPTIONS at build time (see also src/Tools/jEdit/lib/Tools/jedit);
wenzelm [Mon, 09 Sep 2013 13:48:06 +0200] rev 53483
generate application based on $JEDIT_JAVA_OPTIONS $JEDIT_SYSTEM_OPTIONS at build time (see also src/Tools/jEdit/lib/Tools/jedit);
(0) -30000 -10000 -3000 -1000 -300 -100 -30 -10 -1 +1 +10 +30 +100 +300 +1000 +3000 +10000 tip