# HG changeset patch
# User wenzelm
# Date 1451756796 -3600
# Node ID 52a87574bca96bce313c83571333c870d7f6a18d
# Parent  2d150b6afdeb9da1a2c69d15a2a893dc23ffbc71
tuned;

diff -r 2d150b6afdeb -r 52a87574bca9 Admin/lib/Tools/makedist_bundle
--- 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"