14 Jul
2003
14 Jul
'03
8:02 a.m.
On Monday 14 July 2003 12:54 pm, Ross Paterson wrote:
I propose to reverse the defaults for the q and w options, to make quietness the default. Now that Hugs uses the hierarchical libraries, they can produce quite a lot of output. In particular the Hugs banner is often lost.
Sounds reasonable. I don't recall details of exactly what these flags cut off but we should be alert for unintended consequences like losing error messages or warnings (hmmm, does Hugs have warnings?) since their original purposes were something like supporting the hugsserver and being more emacs friendly. -- Alastair