# HG changeset patch
# User wenzelm
# Date 1011626902 -3600
# Node ID c037ff3e5ddf629516e0780ff9086df1faaeb0e6
# Parent  c92128238f85001106cc891a1b1d1aa21ef3c259
save library;

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