# HG changeset patch
# User wenzelm
# Date 850495683 -3600
# Node ID d472c732bc21ffe0f5f98c24da3928faaf6c5e23
# Parent  d1f0505fc60273ce1f0e26111c774b61173eb59f
now discgarb called only for changed databases;

diff -r d1f0505fc602 -r d472c732bc21 lib/scripts/run-polyml
--- a/lib/scripts/run-polyml	Fri Dec 13 17:42:36 1996 +0100
+++ b/lib/scripts/run-polyml	Fri Dec 13 17:48:03 1996 +0100
@@ -45,11 +45,11 @@
 elif [ "$INFILE" -ef "$OUTFILE" ]; then
   DB="$INFILE"
 elif [ -n "$COPYDB" ]; then
-  cp "$INFILE" "$OUTFILE" || fail_out
+  cp -f "$INFILE" "$OUTFILE" || fail_out
   chmod +w "$OUTFILE" || fail_out
   DB="$OUTFILE"
 else
-  [ -f "$OUTFILE" ] && { rm "$OUTFILE" || fail_out }
+  [ -f "$OUTFILE" ] && { rm -f "$OUTFILE" || fail_out }
   echo "PolyML.make_database \"$OUTFILE\"; PolyML.quit();" | $POLY -r "$INFILE"
   [ -f "$OUTFILE" ] || fail_out
   DB="$OUTFILE"
@@ -60,6 +60,7 @@
 ## run it!
 
 START_POLY="$POLY $ML_OPTIONS $DB"
+DB_INFO=$(ls -l $DB)
 
 [ -n "$MLINIT" ] && MLTEXT="$MLINIT $MLTEXT"
 
@@ -74,6 +75,7 @@
   RC=$?
 fi
 
-[ $RC -eq 0 -a -n "$OUTFILE" ] && $DISCGARB "$OUTFILE"
+NEW_DB_INFO=$(ls -l $DB)
+[ $RC -eq 0 -a -n "$OUTFILE" -a "$DB_INFO" != "$NEW_DB_INFO" ] && $DISCGARB "$OUTFILE"
 
 exit $RC