# HG changeset patch
# User wenzelm
# Date 1451747728 -3600
# Node ID 9bb80149dad9590766c5af578f58ceff907afe40
# Parent  773cb226738cd30f9e27cf7291b410e2d83c3a2a
avoid downloading contrib again;

diff -r 773cb226738c -r 9bb80149dad9 Admin/lib/Tools/makedist_bundle
--- a/Admin/lib/Tools/makedist_bundle	Sat Jan 02 15:18:38 2016 +0100
+++ b/Admin/lib/Tools/makedist_bundle	Sat Jan 02 16:15:28 2016 +0100
@@ -83,7 +83,11 @@
 
 init_component "$JEDIT_HOME"
 
-mkdir -p "$ARCHIVE_DIR/contrib"
+if [ -e "$ARCHIVE_DIR/../contrib" ]; then
+  ln -s "../contrib" "$ARCHIVE_DIR/contrib"
+else
+  mkdir -p "$ARCHIVE_DIR/contrib"
+fi
 
 echo "#bundled components" >> "$ISABELLE_TARGET/etc/components"