teeinput
author clasohm
Thu, 01 Jun 1995 13:25:06 +0200
changeset 1141 a94c0ab9a3ed
parent 0 a5a9c433f639
permissions -rwxr-xr-x
commented thms_unifying_with out; placed thm_db into signature again; placed structures ThmDB and Readthy into Pure again; changed init_thy_reader so that thm_db and loaded_thys are preserved (necessary e.g. for ZF)
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 | $*