Merge pull request #5975 from eatkins/ctrl+d

Don't throw ClosedException on ctrl+d
This commit is contained in:
eugene yokota 2020-10-15 14:36:59 -04:00 committed by GitHub
commit 2dc799b2bd
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
1 changed files with 1 additions and 3 deletions

View File

@ -117,9 +117,7 @@ private[sbt] object JLine3 {
}
res match {
case 3 /* ctrl+c */ => throw new ClosedException
case 4 /* ctrl+d */ if term.prompt.render().endsWith(term.prompt.mkPrompt()) =>
throw new ClosedException
case r => r
case r => r
}
}
}