darcs patch: FIX #1378 Add option for a shorter banner on GHCi startup

[Ian Lynagh]

On Fri, Jun 01, 2007 at 07:47:37AM -0600, cdsmith at twu.net wrote:
> Thu May 31 23:36:44 MDT 2007  cdsmith at twu.net
>   * FIX #1378 Add option for a shorter banner on GHCi startup
>   
>   Add -short-ghci-banner and -long-ghci-banner.  The default is long, which is
>   the current behavior.  The short banner prints a one-line introduction with
>   only the version, web site, and ":? for help" message.

Thanks for the patch; I've applied it, but also changed it into a
dynamic flag (and moved some other code around a bit) so that we can
put ":set -short-ghci-banner" in .ghci.

Hopefully this is a good balance between people who like the warmth of
the banner and people who don't want the loss of screen space.


Thanks
Ian