lib/scripts/run-polyml
changeset 12111 d942348d8faf
parent 11485 f7157bdc1e70
child 12810 76f3dd2f151a
--- a/lib/scripts/run-polyml	Fri Nov 09 00:00:53 2001 +0100
+++ b/lib/scripts/run-polyml	Fri Nov 09 00:01:55 2001 +0100
@@ -99,7 +99,7 @@
 ## run it!
 
 if [ -z "$TERMINATE" ]; then
-  FEEDER_OPTS="-s"
+  FEEDER_OPTS=""
 else
   FEEDER_OPTS="-q"
 fi