teeinput
author lcp
Wed, 16 Feb 1994 13:56:20 +0100
changeset 270 d506ea00c825
parent 0 a5a9c433f639
permissions -rwxr-xr-x
tactic/make_elim_preserve: recoded to avoid using lift_inst_rule. Instead instantiate changes the indices of V and W. tactic/cut_inst_tac: new
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     1
#! /bin/sh
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     2
#  teeinput -- start a program and log all inputs to a file
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     3
#     environment variable $LISTEN specifies the file name
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     4
tee -a -i $LISTEN | $*