equal
deleted
inserted
replaced
94 \#* | "") ;; |
94 \#* | "") ;; |
95 *) |
95 *) |
96 COMPONENT="$REPLY" |
96 COMPONENT="$REPLY" |
97 COMPONENT_DIR="$ISABELLE_TARGET/contrib/$COMPONENT" |
97 COMPONENT_DIR="$ISABELLE_TARGET/contrib/$COMPONENT" |
98 case "$COMPONENT" in |
98 case "$COMPONENT" in |
99 jedit_build* | ProofGeneral*) ;; |
99 jedit_build*) ;; |
100 *) |
100 *) |
101 echo " component $COMPONENT" |
101 echo " component $COMPONENT" |
102 CONTRIB="$ARCHIVE_DIR/contrib/${COMPONENT}.tar.gz" |
102 CONTRIB="$ARCHIVE_DIR/contrib/${COMPONENT}.tar.gz" |
103 if [ ! -f "$CONTRIB" ]; then |
103 if [ ! -f "$CONTRIB" ]; then |
104 REMOTE="$ISABELLE_COMPONENT_REPOSITORY/${COMPONENT}.tar.gz" |
104 REMOTE="$ISABELLE_COMPONENT_REPOSITORY/${COMPONENT}.tar.gz" |