teeinput
author clasohm
Tue, 06 Sep 1994 14:44:10 +0200
changeset 586 201e115d8031
parent 0 a5a9c433f639
permissions -rwxr-xr-x
renamed base_on into mk_base and moved it to the beginning of the generated .thy.ML file to make sure that all base theories are present when ML executes the rest of this file
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 | $*