--- a/Admin/lib/Tools/makedist_bundle Sat Jan 02 17:38:00 2016 +0100
+++ b/Admin/lib/Tools/makedist_bundle Sat Jan 02 18:46:36 2016 +0100
@@ -83,10 +83,12 @@
init_component "$JEDIT_HOME"
-if [ -e "$ARCHIVE_DIR/../contrib" ]; then
- ln -s "../contrib" "$ARCHIVE_DIR/contrib"
-else
- mkdir -p "$ARCHIVE_DIR/contrib"
+if [ ! -e "$ARCHIVE_DIR/contrib" ]; then
+ if [ ! -e "$ARCHIVE_DIR/../contrib" ]; then
+ mkdir -p "$ARCHIVE_DIR/contrib"
+ else
+ ln -s "../contrib" "$ARCHIVE_DIR/contrib"
+ fi
fi
echo "#bundled components" >> "$ISABELLE_TARGET/etc/components"