Flush output after progress bars

Should fix some progress info not being cleared
2026-08-22 14:17:13 +02:00 · 2017-02-21 15:57:39 +01:00
parent 9ece419bc8
commit 21ba9888a5
1 changed files with 2 additions and 0 deletions
@@ -348,6 +348,8 @@ object TermDisplay {
      }
      for (_ <- 0 until currentHeight)
        out.up(2)
      out.flush()
    }
    private var previous = Set.empty[String]