mirror of
https://github.com/CrystalSplitter/ghcitui.git
synced 2024-09-11 10:55:29 +03:00
This is mostly to replace the now missing scrollbar. The scrollbar is neat, but for now I consider it solely aesthetic and the real info we want is the total line count and the current position percentage. |
||
---|---|---|
.. | ||
AppConfig.hs | ||
AppInterpState.hs | ||
AppState.hs | ||
AppTopLevel.hs | ||
BrickUI.hs | ||
DrawSourceViewer.hs | ||
Events.hs | ||
HelpText.hs | ||
Main.hs | ||
SourceWindow.hs | ||
Util.hs |