diff -r c92128238f85 -r c037ff3e5ddf Admin/makebin --- a/Admin/makebin Mon Jan 21 16:15:16 2002 +0100 +++ b/Admin/makebin Mon Jan 21 16:28:22 2002 +0100 @@ -137,6 +137,7 @@ if [ -n "$DO_LIBRARY" ]; then "$TAR" cf "${ISABELLE_NAME}_library.tar" $ISABELLE_NAME/browser_info && \ gzip -f "${ISABELLE_NAME}_library.tar" + cp -f "${ISABELLE_NAME}_library.tar.gz" "$ARCHIVE_DIR" fi done