# HG changeset patch
# User wenzelm
# Date 1718117300 -7200
# Node ID 8365f1e7955e1b73c5fe172f7e6f533f9fb62456
# Parent  5a555acad203f8d8fbbb8be2811f2d48e742f8be
minor performance tuning;

diff -r 5a555acad203 -r 8365f1e7955e src/Pure/General/bytes.scala
--- a/src/Pure/General/bytes.scala	Tue Jun 11 16:39:53 2024 +0200
+++ b/src/Pure/General/bytes.scala	Tue Jun 11 16:48:20 2024 +0200
@@ -20,14 +20,12 @@
 object Bytes {
   val empty: Bytes = new Bytes(Array[Byte](), 0, 0)
 
-  def apply(s: CharSequence): Bytes = {
-    val str = s.toString
-    if (str.isEmpty) empty
+  def apply(s: CharSequence): Bytes =
+    if (s.isEmpty) empty
     else {
-      val b = UTF8.bytes(str)
+      val b = UTF8.bytes(s.toString)
       new Bytes(b, 0, b.length)
     }
-  }
 
   def apply(a: Array[Byte]): Bytes = apply(a, 0, a.length)