FIX #1378 Add option for a shorter banner on GHCi startup
authorcdsmith@twu.net <unknown>
Fri, 1 Jun 2007 05:36:44 +0000 (05:36 +0000)
committercdsmith@twu.net <unknown>
Fri, 1 Jun 2007 05:36:44 +0000 (05:36 +0000)
commitd061166982c65f8e61b4faf942bc5737da2b272c
treeb234aad50a2a1a92947cac8cba1ff0286147c2d7
parent2506fbadd58a464e4c6d63375b909d853b99b087
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.
compiler/ghci/InteractiveUI.hs
compiler/main/Main.hs
compiler/main/StaticFlags.hs
docs/users_guide/flags.xml