diff -r 7212040b71f2 -r 4bc08baa3fbb lib/scripts/run-polyml
--- a/lib/scripts/run-polyml	Tue Jun 14 22:08:53 2005 +0200
+++ b/lib/scripts/run-polyml	Tue Jun 14 22:19:32 2005 +0200
@@ -57,7 +57,6 @@
   export POLYPATH="$(fixpath "$(dirname "$ML_DBASE")")"
 fi
 
-DISCGARB="$POLY"
 DISCGARB_OPTIONS="-d -c"
 
 EXIT="fun exit 0 = (OS.Process.exit OS.Process.success): unit | exit _ = OS.Process.exit OS.Process.failure;"
@@ -116,7 +115,7 @@
 
 NEW_DB_INFO="$(ls -l "$DB" 2>/dev/null)"
 [ -n "$OUTFILE" -a -n "$COMPRESS" -a "$DB_INFO" != "$NEW_DB_INFO" ] && \
-  "$DISCGARB" $DISCGARB_OPTIONS "$OUTFILE"
+  "$POLY" $DISCGARB_OPTIONS "$OUTFILE"
 [ -n "$OUTFILE" -a -f "$OUTFILE" -a -n "$NOWRITE" ] && chmod -w "$OUTFILE"
 
 exit "$RC"