# HG changeset patch
# User wenzelm
# Date 957969805 -7200
# Node ID 0a129bdd77d7a2fd788e7a96d222a796e4ea7cc6
# Parent  d816ec3fab28f08702af0c5dac51fd6c1a138613
polyml;

diff -r d816ec3fab28 -r 0a129bdd77d7 Admin/filesizes
--- 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 ]