author | wenzelm |
Wed, 10 May 2000 16:43:25 +0200 | |
changeset 8852 | 0a129bdd77d7 |
parent 8851 | d816ec3fab28 |
child 8853 | 079f607dc3dd |
Admin/filesizes | file | annotate | diff | comparison | revisions |
--- a/Admin/filesizes Wed May 10 16:43:10 2000 +0200 +++ b/Admin/filesizes Wed May 10 16:43:25 2000 +0200 @@ -76,7 +76,7 @@ fi if [ $# -eq 0 -o "$1" = "-rpm" ]; then - RPM_SML_SIZE=$[ $(wc -c < rpm/smlnj-110.0-3.i386.rpm) / 1024 ] + RPM_SML_SIZE=$[ $(wc -c < rpm/polyml-3X-1.i386.rpm) / 1024 ] RPM_BASE_SIZE=$[ $(wc -c < rpm/isabelle.rpm) / 1024 ] RPM_HOL_SIZE=$[ $(wc -c < rpm/isabelle-HOL.i386.rpm) / 1024 ] RPM_REAL_SIZE=$[ $(wc -c < rpm/isabelle-HOL-Real.i386.rpm) / 1024 ]