diff -r ddbaf6785d0d -r 4caa07322d8f src/Tools/teeinput
--- a/src/Tools/teeinput	Thu Oct 07 12:38:12 1999 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,4 +0,0 @@
-#! /bin/sh
-#  teeinput -- start a program and log all inputs to a file
-#     environment variable $LISTEN specifies the file name
-tee -a -i $LISTEN | $*