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

[Chris Smith]

Simon Marlow wrote:
> Wow, that patch was nearly 0.5Mb.  Can we do something about the
> patch size?

I just did a darcs send.  Should I do something different?

> 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?

Personally, I actually rather like the current banner.  I just did this 
because I'm trying to get familiar with the code, and this was the easiest 
thing on trac.  I'd hate to lose my ASCII art GHCi banner because of it!

-- 
Chris Smith