| changeset 53485 | a837df2ceee5 |
| parent 53484 | 1100982a071c |
| child 53488 | 009d3bcf6907 |
--- 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"