[ "$ML_SYSTEM" = polyml-4.1.1 ] && DISCGARB_OPTIONS="$DISCGARB_OPTIONS -S 120";
authorwenzelm
Wed, 08 Aug 2001 15:16:38 +0200
changeset 11485 f7157bdc1e70
parent 11484 44053d894713
child 11486 8f32860eac3a
[ "$ML_SYSTEM" = polyml-4.1.1 ] && DISCGARB_OPTIONS="$DISCGARB_OPTIONS -S 120";
lib/scripts/run-polyml
--- a/lib/scripts/run-polyml	Wed Aug 08 14:57:22 2001 +0200
+++ b/lib/scripts/run-polyml	Wed Aug 08 15:16:38 2001 +0200
@@ -73,6 +73,7 @@
   check_file "$ML_DBASE_PREFIX$ML_DBASE"
   INFILE="$ML_DBASE"
   MLTEXT="val use = PolyML.use; $EXIT $MLTEXT"
+  [ "$ML_SYSTEM" = polyml-4.1.1 ] && DISCGARB_OPTIONS="$DISCGARB_OPTIONS -S 120"
 else
   COPYDB=true
 fi