# HG changeset patch
# User wenzelm
# Date 1520602518 -3600
# Node ID bb2bbabf3d37724987ba508328c557d327640299
# Parent  f8037c7e465977278144e8ffc3dc5fd5a295df4f
clarified initial protocol;

diff -r f8037c7e4659 -r bb2bbabf3d37 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 _ =>
     }
   }