save library;
authorwenzelm
Mon, 21 Jan 2002 16:28:22 +0100
changeset 12830 c037ff3e5ddf
parent 12829 c92128238f85
child 12831 a2a3896f9c48
save library;
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