lib/scripts/run-polyml
changeset 3503 390093b95cb0
parent 3055 5da4afa207ad
child 4333 1d326b826851
equal deleted inserted replaced
3502:ec22ba0a26ec 3503:390093b95cb0
     2 #
     2 #
     3 # $Id$
     3 # $Id$
     4 #
     4 #
     5 # Poly/ML startup script.
     5 # Poly/ML startup script.
     6 #
     6 #
     7 # Global vars: INFILE OUTFILE MLTEXT TERMINATE,
     7 # Global vars: INFILE OUTFILE MLTEXT TERMINATE NOWRITE,
     8 # and from settings
     8 # and from settings
     9 
     9 
    10 
    10 
    11 ## diagnostics
    11 ## diagnostics
    12 
    12 
    73   RC=$?
    73   RC=$?
    74 fi
    74 fi
    75 
    75 
    76 NEW_DB_INFO=$(ls -l "$DB")
    76 NEW_DB_INFO=$(ls -l "$DB")
    77 [ -n "$OUTFILE" -a "$DB_INFO" != "$NEW_DB_INFO" ] && $DISCGARB "$OUTFILE"
    77 [ -n "$OUTFILE" -a "$DB_INFO" != "$NEW_DB_INFO" ] && $DISCGARB "$OUTFILE"
       
    78 [ -n "$OUTFILE" -a -n "$NOWRITE" ] && chmod -w "$OUTFILE"
    78 
    79 
    79 exit $RC
    80 exit $RC