diff -r 5ed72705c201 -r 2f39aa4bebf3 lib/scripts/feeder
--- a/lib/scripts/feeder	Tue Dec 30 13:43:39 1997 +0100
+++ b/lib/scripts/feeder	Wed Dec 31 15:17:49 1997 +0100
@@ -17,7 +17,6 @@
   echo
   echo "  Options are:"
   echo "    -h TEXT      head text"
-  echo "    -i           ignore INT signal"
   echo "    -p           emit my pid"
   echo "    -q           do not pipe stdin"
   echo "    -s           filter symbols"
@@ -40,21 +39,17 @@
 # options
 
 HEAD=""
-NOINT=""
 EMITPID=""
 QUIT=""
 SYMBOLS=""
 TAIL=""
 
-while getopts "h:ipqst:" OPT
+while getopts "h:pqst:" OPT
 do
   case "$OPT" in
     h)
       HEAD="$OPTARG"
       ;;
-    i)
-      NOINT=true
-      ;;
     p)
       EMITPID=true
       ;;
@@ -84,4 +79,4 @@
 
 ## main
 
-exec perl -w $DIR/feeder.pl "$HEAD" "$NOINT" "$EMITPID" "$QUIT" "$SYMBOLS" "$TAIL"
+exec perl -w $DIR/feeder.pl "$HEAD" "$EMITPID" "$QUIT" "$SYMBOLS" "$TAIL"