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

[Ian Lynagh]

On Fri, Jun 01, 2007 at 07:55:59AM -0600, Chris Smith wrote:
> 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?

No, that is right.

There are several tags in the context of your patch, so I assume darcs
just got confused for some reason.


Thanks
Ian