teeinput
author wenzelm
Mon, 24 Jan 1994 12:03:53 +0100
changeset 247 bc10568855ee
parent 0 a5a9c433f639
permissions -rwxr-xr-x
added is_empty: env -> bool, minidx: env -> int option;

#! /bin/sh
#  teeinput -- start a program and log all inputs to a file
#     environment variable $LISTEN specifies the file name
tee -a -i $LISTEN | $*