# HG changeset patch
# User wenzelm
# Date 1520602213 -3600
# Node ID f8037c7e465977278144e8ffc3dc5fd5a295df4f
# Parent  82c5ca89ac61e1e66a20bff45d48059c885563bf
ignore empty lines;

diff -r 82c5ca89ac61 -r f8037c7e4659 src/Pure/Tools/server.scala
--- a/src/Pure/Tools/server.scala	Fri Mar 09 14:26:08 2018 +0100
+++ b/src/Pure/Tools/server.scala	Fri Mar 09 14:30:13 2018 +0100
@@ -230,7 +230,7 @@
         while (!finished) {
           connection.read_line() match {
             case None => finished = true
-            case Some(line) =>
+            case Some(line) if line != "" =>
               val (cmd, input) = Server.split_line(line)
               Server.commands.get(cmd) match {
                 case None => connection.reply_error("Bad command " + quote(cmd))