equal
deleted
inserted
replaced
135 cp -f "${IMG}_$PLATFORM.tar.gz" "$ARCHIVE_DIR" |
135 cp -f "${IMG}_$PLATFORM.tar.gz" "$ARCHIVE_DIR" |
136 |
136 |
137 if [ -n "$DO_LIBRARY" ]; then |
137 if [ -n "$DO_LIBRARY" ]; then |
138 "$TAR" cf "${ISABELLE_NAME}_library.tar" $ISABELLE_NAME/browser_info && \ |
138 "$TAR" cf "${ISABELLE_NAME}_library.tar" $ISABELLE_NAME/browser_info && \ |
139 gzip -f "${ISABELLE_NAME}_library.tar" |
139 gzip -f "${ISABELLE_NAME}_library.tar" |
|
140 cp -f "${ISABELLE_NAME}_library.tar.gz" "$ARCHIVE_DIR" |
140 fi |
141 fi |
141 done |
142 done |
142 |
143 |
143 |
144 |
144 # clean up |
145 # clean up |