--- a/src/Pure/Tools/server.scala Fri Mar 09 14:30:13 2018 +0100
+++ b/src/Pure/Tools/server.scala Fri Mar 09 14:35:18 2018 +0100
@@ -223,9 +223,8 @@
private def handle(connection: Server.Connection)
{
connection.read_line() match {
- case None =>
- case Some(line) if line != password => connection.reply_error("Bad protocol")
- case _ =>
+ case Some(line) if line == password =>
+ connection.reply_ok(JSON.empty)
var finished = false
while (!finished) {
connection.read_line() match {
@@ -253,6 +252,7 @@
case _ =>
}
}
+ case _ =>
}
}