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