do not register quasi-components, notably cygwin;
authorwenzelm
Mon, 14 Jan 2013 20:12:18 +0100
changeset 50891 d1a0335b4231
parent 50890 097e38daa03a
child 50892 9a7d81d66d09
do not register quasi-components, notably cygwin;
Admin/lib/Tools/makedist_bundles
--- 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
             ;;