author | wenzelm |
Fri, 09 Mar 2018 13:11:47 +0100 | |
changeset 67792 | 73c7a55972b4 |
parent 67791 | acecef5fad58 |
child 67793 | d0eeaeab48cc |
--- a/src/Pure/Tools/server.scala Fri Mar 09 13:07:00 2018 +0100 +++ b/src/Pure/Tools/server.scala Fri Mar 09 13:11:47 2018 +0100 @@ -215,8 +215,7 @@ { connection.read_line() match { case None => - case Some(line) if line != password => - connection.reply_error("Bad password -- connection closed") + case Some(line) if line != password => connection.reply_error("Bad protocol") case _ => var finished = false while (!finished) {