lib/scripts/run-polyml
changeset 2936 bd33e7aae062
parent 2605 1effe7413486
child 3007 e5efa177ee0c
--- a/lib/scripts/run-polyml	Fri Apr 11 15:21:36 1997 +0200
+++ b/lib/scripts/run-polyml	Fri Apr 11 17:30:15 1997 +0200
@@ -44,12 +44,12 @@
 elif [ "$INFILE" -ef "$OUTFILE" ]; then
   DB="$INFILE"
 elif [ -n "$COPYDB" ]; then
-  [ -f "$OUTFILE" ] && { rm -f "$OUTFILE" || fail_out }
+  [ -f "$OUTFILE" ] && { rm -f "$OUTFILE" || fail_out; }
   cp "$INFILE" "$OUTFILE" || fail_out
   chmod +w "$OUTFILE" || fail_out
   DB="$OUTFILE"
 else
-  [ -f "$OUTFILE" ] && { rm -f "$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"