xlisten
author lcp
Mon Dec 13 18:50:03 1993 +0100 (1993-12-13)
changeset 196 7646f5b4653c
parent 0 a5a9c433f639
permissions -rwxr-xr-x
added isabelle-users paragraph
     1 #! /bin/sh
     2 #  xlisten -- start a program in one window and create a listener window
     3 #     environment variable $LISTEN specifies the file name
     4 
     5 #create the file!
     6 date > $LISTEN
     7 
     8 xterm -geo 80x10+0+0 -T Listener -n Listener -e tail -f $LISTEN &
     9 sleep 2
    10 xterm -geo 80x45+0-0 -e teeinput $* &