src/Tools/teeinput
author paulson
Tue, 16 Jul 1996 15:49:46 +0200
changeset 1868 836950047d85
parent 0 a5a9c433f639
child 2774 4b7b38765619
permissions -rwxr-xr-x
Put in minimal simpset to avoid excessive simplification, just as in revision 1.9 of HOL/indrule.ML

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