Admin/makebin
changeset 12830 c037ff3e5ddf
parent 12827 05c13f5a515d
child 12985 9db054a40247
equal deleted inserted replaced
12829:c92128238f85 12830:c037ff3e5ddf
   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