clarified initial protocol;
authorwenzelm
Fri, 09 Mar 2018 14:35:18 +0100
changeset 67796 bb2bbabf3d37
parent 67795 f8037c7e4659
child 67797 1cfc7541012e
clarified initial protocol;
src/Pure/Tools/server.scala
--- 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 _ =>
     }
   }