From 993af6da95b81b2b361c5649e58a240bc91fb205 Mon Sep 17 00:00:00 2001 From: Davy Landman Date: Thu, 2 Jan 2025 21:17:13 +0100 Subject: [PATCH] Cherry-picking the fix in 4c14ae6 --- src/org/rascalmpl/repl/TerminalProgressBarMonitor.java | 2 -- 1 file changed, 2 deletions(-) diff --git a/src/org/rascalmpl/repl/TerminalProgressBarMonitor.java b/src/org/rascalmpl/repl/TerminalProgressBarMonitor.java index 63874c5d76..5f0912e69d 100644 --- a/src/org/rascalmpl/repl/TerminalProgressBarMonitor.java +++ b/src/org/rascalmpl/repl/TerminalProgressBarMonitor.java @@ -531,9 +531,7 @@ public synchronized int jobEnd(String name, boolean succeeded) { if (pb != null && --pb.nesting == -1) { eraseBars(); - // write it one last time into the scrollback buffer (on top) pb.done(); - pb.write(); bars.remove(pb); // print the left over bars under this one. printBars();