src/Tools/teeinput
author nipkow
Fri, 24 Oct 1997 18:10:51 +0200
changeset 4003 2bbeed529077
parent 2774 4b7b38765619
permissions -rwxr-xr-x
Added goal Set.thy "(Union M = {}) = (! A : M. A = {})"; AddIffs [Union_empty_conv]; Good idea??

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