mirror of
https://github.com/jtdaugherty/brick.git
synced 2024-11-29 02:33:11 +03:00
keybindEventHelpWidget: slightly improve formatting of "comments"
This commit is contained in:
parent
286c88b137
commit
4884df8aa6
@ -144,7 +144,7 @@ keybindEventHelpWidget (evName, desc, evs) =
|
||||
getText (Comment s) = s
|
||||
getText (Verbatim s) = s
|
||||
label = case evName of
|
||||
Comment s -> txt $ "; " <> s
|
||||
Comment s -> txt s -- TODO: was "; " <> s
|
||||
Verbatim s -> txt s -- TODO: was: emph $ txt s
|
||||
in padBottom (Pad 1) $
|
||||
vBox [ txt desc
|
||||
|
Loading…
Reference in New Issue
Block a user