--- a/Admin/lib/Tools/makedist_bundles Mon Jan 14 19:45:14 2013 +0100
+++ b/Admin/lib/Tools/makedist_bundles Mon Jan 14 20:12:18 2013 +0100
@@ -75,6 +75,7 @@
\#* | "") ;;
*)
COMPONENT="$REPLY"
+ COMPONENT_DIR="$ISABELLE_TARGET/contrib/$COMPONENT"
case "$COMPONENT" in
jedit_build*) ;;
*)
@@ -88,7 +89,10 @@
fi
tar -C "$ISABELLE_TARGET/contrib" -x -z -f "$CONTRIB"
- echo "contrib/$COMPONENT" >> "$ISABELLE_TARGET/etc/components"
+ if [ -f "$COMPONENT_DIR/etc/settings" -o -f "$COMPONENT_DIR/etc/components" ]
+ then
+ echo "contrib/$COMPONENT" >> "$ISABELLE_TARGET/etc/components"
+ fi
;;
esac
;;