lib/scripts/run-polyml
changeset 2936 bd33e7aae062
parent 2605 1effe7413486
child 3007 e5efa177ee0c
equal deleted inserted replaced
2935:998cb95fdd43 2936:bd33e7aae062
    42   DB="$INFILE"
    42   DB="$INFILE"
    43   ML_OPTIONS="-r $ML_OPTIONS"  
    43   ML_OPTIONS="-r $ML_OPTIONS"  
    44 elif [ "$INFILE" -ef "$OUTFILE" ]; then
    44 elif [ "$INFILE" -ef "$OUTFILE" ]; then
    45   DB="$INFILE"
    45   DB="$INFILE"
    46 elif [ -n "$COPYDB" ]; then
    46 elif [ -n "$COPYDB" ]; then
    47   [ -f "$OUTFILE" ] && { rm -f "$OUTFILE" || fail_out }
    47   [ -f "$OUTFILE" ] && { rm -f "$OUTFILE" || fail_out; }
    48   cp "$INFILE" "$OUTFILE" || fail_out
    48   cp "$INFILE" "$OUTFILE" || fail_out
    49   chmod +w "$OUTFILE" || fail_out
    49   chmod +w "$OUTFILE" || fail_out
    50   DB="$OUTFILE"
    50   DB="$OUTFILE"
    51 else
    51 else
    52   [ -f "$OUTFILE" ] && { rm -f "$OUTFILE" || fail_out }
    52   [ -f "$OUTFILE" ] && { rm -f "$OUTFILE" || fail_out; }
    53   echo "PolyML.make_database \"$OUTFILE\"; PolyML.quit();" | $POLY -r "$INFILE"
    53   echo "PolyML.make_database \"$OUTFILE\"; PolyML.quit();" | $POLY -r "$INFILE"
    54   [ -f "$OUTFILE" ] || fail_out
    54   [ -f "$OUTFILE" ] || fail_out
    55   DB="$OUTFILE"
    55   DB="$OUTFILE"
    56   MLINIT="$MLINIT init_database ();"
    56   MLINIT="$MLINIT init_database ();"
    57 fi
    57 fi