equal
deleted
inserted
replaced
91 chmod -R g=o "$TMP" |
91 chmod -R g=o "$TMP" |
92 chgrp -R isabelle "$TMP" |
92 chgrp -R isabelle "$TMP" |
93 |
93 |
94 for IMG in HOL HOL-Real ZF |
94 for IMG in HOL HOL-Real ZF |
95 do |
95 do |
96 "$TAR" cf "${IMG}_$PLATFORM.tar" "$ISABELLE_NAME/heaps/$COMPILER/$IMG" |
96 "$TAR" cf "${IMG}_$PLATFORM.tar" \ |
|
97 "$ISABELLE_NAME/heaps/$COMPILER/$IMG" \ |
|
98 "$ISABELLE_NAME/heaps/$COMPILER/log/$IMG.gz" |
97 gzip "${IMG}_$PLATFORM.tar" |
99 gzip "${IMG}_$PLATFORM.tar" |
98 cp -f "${IMG}_$PLATFORM.tar.gz" "$ARCHIVE_DIR" |
100 cp -f "${IMG}_$PLATFORM.tar.gz" "$ARCHIVE_DIR" |
99 done |
101 done |
100 |
102 |
101 |
103 |