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

[Simon Marlow]

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.

Wow, that patch was nearly 0.5Mb.  Can we do something about the patch size?

Regarding the patch itself, I'd rather just kill the current banner and replace 
it with a shorter banner if we're going to do this.  What does everyone else think?

Cheers,
	Simon