--- 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 | $*