Skip to content

Commit

Permalink
Improve terminal size warning message
Browse files Browse the repository at this point in the history
  • Loading branch information
thezbm committed Jan 30, 2025
1 parent 731259e commit deb9fdc
Showing 1 changed file with 6 additions and 2 deletions.
8 changes: 6 additions & 2 deletions lib/tui/tui.ml
Original file line number Diff line number Diff line change
Expand Up @@ -49,8 +49,12 @@ let get_terminal_dimensions () =
| Some height, Some width ->
if !size_warning && (height < min_height || width < min_width) then (
Printf.printf
"⚠️ Terminal size is too small! Expected minimum size: %d x %d, but \
got: %d x %d.\n"
{|⚠️ Terminal size is too small! GitHub TUI works better on bigger terminals.
Expected size: %3d width x %3d height
But got: %3d width x %3d height

Pass the --ignore-size-warning flag to run anyway.
|}
min_width min_height width height;
exit 1);
{ height; width }
Expand Down

0 comments on commit deb9fdc

Please sign in to comment.