# HG changeset patch
# User wenzelm
# Date 1378730896 -7200
# Node ID a837df2ceee5bce7afe07a758b97f4ebdf728d9d
# Parent  1100982a071cf77b61b27034aeb1d55523b17b73
override potential changes in $ISABELLE_HOME_USER/etc/settings;

diff -r 1100982a071c -r a837df2ceee5 Admin/lib/Tools/makedist_bundle
--- a/Admin/lib/Tools/makedist_bundle	Mon Sep 09 14:22:39 2013 +0200
+++ b/Admin/lib/Tools/makedist_bundle	Mon Sep 09 14:48:16 2013 +0200
@@ -53,6 +53,8 @@
 
 # bundled components
 
+init_component "$JEDIT_HOME"
+
 mkdir -p "$ARCHIVE_DIR/contrib"
 
 echo "#bundled components" >> "$ISABELLE_TARGET/etc/components"