# HG changeset patch
# User kleing
# Date 1052216989 -7200
# Node ID 46ad7fd03a38fc480d97830469de630adf01a864
# Parent  bfca18e9ab72a698ef092b5c2845bc001dac5f33
use -Smax with poly 4.1.3 for maximum database space (see poly release notes)

diff -r bfca18e9ab72 -r 46ad7fd03a38 lib/scripts/run-polyml
--- a/lib/scripts/run-polyml	Tue May 06 10:47:17 2003 +0200
+++ b/lib/scripts/run-polyml	Tue May 06 12:29:49 2003 +0200
@@ -73,6 +73,8 @@
   check_file "$ML_DBASE_PREFIX$ML_DBASE"
   INFILE="$ML_DBASE"
   MLTEXT="val use = PolyML.use; $EXIT $MLTEXT"
+  [ "$ML_SYSTEM" = polyml-4.1.3 ] && \
+    DISCGARB_OPTIONS="$DISCGARB_OPTIONS -Smax"
   [ "$ML_SYSTEM" = polyml-4.1.1 -o "$ML_SYSTEM" = polyml-4.1.2 ] && \
     DISCGARB_OPTIONS="$DISCGARB_OPTIONS -S 180"
 else
@@ -111,6 +113,7 @@
   { read FPID; "$POLY" $ML_OPTIONS "$DB"; RC="$?"; kill -HUP "$FPID"; exit "$RC"; }
 RC="$?"
 
+
 NEW_DB_INFO=$(ls -l "$DB" 2>/dev/null)
 [ -n "$OUTFILE" -a -n "$COMPRESS" -a "$DB_INFO" != "$NEW_DB_INFO" ] && \
   "$DISCGARB" $DISCGARB_OPTIONS "$OUTFILE"