changeset 10113 | a1f8d7d4084b |
parent 10101 | 746263fbcbfd |
child 10307 | 0df0bbd7e324 |
--- a/Admin/makebin Thu Sep 28 19:10:19 2000 +0200 +++ b/Admin/makebin Thu Sep 28 23:00:11 2000 +0200 @@ -93,7 +93,9 @@ for IMG in HOL HOL-Real ZF do - "$TAR" cf "${IMG}_$PLATFORM.tar" "$ISABELLE_NAME/heaps/$COMPILER/$IMG" + "$TAR" cf "${IMG}_$PLATFORM.tar" \ + "$ISABELLE_NAME/heaps/$COMPILER/$IMG" \ + "$ISABELLE_NAME/heaps/$COMPILER/log/$IMG.gz" gzip "${IMG}_$PLATFORM.tar" cp -f "${IMG}_$PLATFORM.tar.gz" "$ARCHIVE_DIR" done