proposed UI change

Ross Paterson ross@soi.city.ac.uk
Mon, 14 Jul 2003 12:54:40 +0100


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.