author | wenzelm |
Mon, 21 Jan 2002 16:28:22 +0100 | |
changeset 12830 | c037ff3e5ddf |
parent 12829 | c92128238f85 |
child 12831 | a2a3896f9c48 |
Admin/makebin | file | annotate | diff | comparison | revisions |
--- 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