Merge pull request #6022 from eatkins/network-flush

Flush terminal output stream after readline
This commit is contained in:
Ethan Atkins 2020-10-24 19:58:26 -07:00 committed by GitHub
commit b5fc17cc7a
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
1 changed files with 1 additions and 0 deletions

View File

@ -565,6 +565,7 @@ final class NetworkChannel(
logShutdown: Boolean,
remainingCommands: Option[(String, String)]
): Unit = {
doFlush()
terminal.close()
StandardMain.exchange.removeChannel(this)
super.shutdown(logShutdown)