lib/scripts/run-polyml
changeset 12111 d942348d8faf
parent 11485 f7157bdc1e70
child 12810 76f3dd2f151a
equal deleted inserted replaced
12110:f8b4b11cd79d 12111:d942348d8faf
    97 
    97 
    98 
    98 
    99 ## run it!
    99 ## run it!
   100 
   100 
   101 if [ -z "$TERMINATE" ]; then
   101 if [ -z "$TERMINATE" ]; then
   102   FEEDER_OPTS="-s"
   102   FEEDER_OPTS=""
   103 else
   103 else
   104   FEEDER_OPTS="-q"
   104   FEEDER_OPTS="-q"
   105 fi
   105 fi
   106 
   106 
   107 DB_INFO=$(ls -l "$DB" 2>/dev/null)
   107 DB_INFO=$(ls -l "$DB" 2>/dev/null)