author | wenzelm |
Sat, 02 Jan 2016 16:15:28 +0100 | |
changeset 62037 | 9bb80149dad9 |
parent 62036 | 773cb226738c |
child 62038 | 5651de00bca9 |
--- 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"