# HG changeset patch
# User wenzelm
# Date 1720521665 -7200
# Node ID 769a52499f12158002f03be4eb9a0e6cb66955cb
# Parent  d1662f1296dbcc583eb15139bb6ca9a20e6b84f5
tuned;

diff -r d1662f1296db -r 769a52499f12 src/Pure/PIDE/byte_message.scala
--- a/src/Pure/PIDE/byte_message.scala	Tue Jul 09 12:32:33 2024 +0200
+++ b/src/Pure/PIDE/byte_message.scala	Tue Jul 09 12:41:05 2024 +0200
@@ -44,7 +44,7 @@
           builder += c.toByte
         }
       }
-    if (c == -1 && line.size == 0) None else Some(line.trim_line)
+    if (c == -1 && line.is_empty) None else Some(line.trim_line)
   }