teeinput
author lcp
Tue, 05 Oct 1993 15:21:29 +0100
changeset 25 3ac1c0c0016e
parent 0 a5a9c433f639
permissions -rwxr-xr-x
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many changes epsilon,arith: many changes ordinal/succ_mem_succI/E: deleted; use succ_leI/E nat/nat_0_in_succ: deleted; use nat_0_le univ/Vset_rankI: deleted; use VsetI

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