optional jedit_build/etc/user-settings enable to override defaults produced by late component initialization;
--- a/src/Tools/jEdit/jedit_build/Tools/jedit Sat May 21 00:09:18 2011 +0200
+++ b/src/Tools/jEdit/jedit_build/Tools/jedit Sat May 21 11:31:59 2011 +0200
@@ -134,6 +134,8 @@
set -o allexport
init_component "$TARGET_DIR"
+[ -f "$ISABELLE_JEDIT_BUILD_HOME/etc/user-settings" ] && \
+ source "$ISABELLE_JEDIT_BUILD_HOME/etc/user-settings"
set +o allexport
exec "$TARGET_DIR/lib/Tools/jedit" "$@"