Here goes nothing..

C.Reinke C.Reinke@ukc.ac.uk
Thu, 30 May 2002 17:07:48 +0100


> Thanks for reporting this; now fixed.
> 
> --sigbjorn

Thanks for fixing;
as usual, I'm impressed by this efficiency!-)

Btw, is there a way to indicate end-of-input in Hugs?

In typical shells, that would be CTRL-D, and makes things
like the "cat >script" work at the prompt (and it doesn't
end the shell if there is a nested process waiting for input).

Claus