diff -r f8b4b11cd79d -r d942348d8faf lib/scripts/feeder
--- a/lib/scripts/feeder	Fri Nov 09 00:00:53 2001 +0100
+++ b/lib/scripts/feeder	Fri Nov 09 00:01:55 2001 +0100
@@ -21,7 +21,6 @@
   echo "    -h TEXT      head text"
   echo "    -p           emit my pid"
   echo "    -q           do not pipe stdin"
-  echo "    -s           filter symbols"
   echo "    -t TEXT      tail text"
   echo
   echo "  Output texts (pid, head, stdin, tail), then wait to be terminated."
@@ -43,10 +42,9 @@
 HEAD=""
 EMITPID=""
 QUIT=""
-SYMBOLS=""
 TAIL=""
 
-while getopts "h:pqst:" OPT
+while getopts "h:pqt:" OPT
 do
   case "$OPT" in
     h)
@@ -58,9 +56,6 @@
     q)
       QUIT=true
       ;;
-    s)
-      SYMBOLS=true
-      ;;
     t)
       TAIL="$OPTARG"
       ;;
@@ -84,4 +79,4 @@
 #set by configure
 AUTO_PERL=perl
 
-exec "$AUTO_PERL" -w "$DIR"/feeder.pl "$HEAD" "$EMITPID" "$QUIT" "$SYMBOLS" "$TAIL"
+exec "$AUTO_PERL" -w "$DIR"/feeder.pl "$HEAD" "$EMITPID" "$QUIT" "$TAIL"