# HG changeset patch
# User wenzelm
# Date 1305970319 -7200
# Node ID 7438ee56b89a43a05ad3427fac3589df3d6d4b65
# Parent  4b127cc20aac3ce6454e066cdc2e2a4e9d755cdc
optional jedit_build/etc/user-settings enable to override defaults produced by late component initialization;

diff -r 4b127cc20aac -r 7438ee56b89a src/Tools/jEdit/jedit_build/Tools/jedit
--- 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" "$@"