Merge pull request bcpierce00#927 from tleedjarv/terminated

Improve the TUI output when interrupted
bogusbul · May 28, 2023 · 42a0736 · 42a0736
2 parents 5561201 + 5102ddd
commit 42a0736
Showing 1 changed file with 3 additions and 0 deletions.
diff --git a/src/uitext.ml b/src/uitext.ml
@@ -1581,6 +1581,9 @@ let getProfile default =
   !selection
 
 let handleException e =
+  (* Keep the current status line (if any) and don't repeat it any more *)
+  alwaysDisplay "\n";
+  Util.set_infos "";
   restoreTerminal();
   let msg = Uicommon.exn2string e in
   let () =