From deb9fdc6befbc22c616ea7dfa6c1c46566c632f9 Mon Sep 17 00:00:00 2001
From: Beiming Zhang <thebeimingzhang@outlook.com>
Date: Thu, 30 Jan 2025 18:34:10 +0800
Subject: [PATCH] Improve terminal size warning message

---
 lib/tui/tui.ml | 8 ++++++--
 1 file changed, 6 insertions(+), 2 deletions(-)

diff --git a/lib/tui/tui.ml b/lib/tui/tui.ml
index fd9a8c5..049b547 100644
--- a/lib/tui/tui.ml
+++ b/lib/tui/tui.ml
@@ -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 }