# HG changeset patch
# User wenzelm
# Date 1679835728 -7200
# Node ID be0b9396604ef58bee5e45cff406ac74864e84d7
# Parent  0d6e592d24c06066b6a03be404c29a78aedbe7a8
tuned;

diff -r 0d6e592d24c0 -r be0b9396604e src/Pure/General/bytes.scala
--- a/src/Pure/General/bytes.scala	Sun Mar 26 14:45:28 2023 +0200
+++ b/src/Pure/General/bytes.scala	Sun Mar 26 15:02:08 2023 +0200
@@ -202,10 +202,12 @@
   }
 
   def trim_line: Bytes =
-    if (length >= 2 && charAt(length - 2) == 13 && charAt(length - 1) == 10)
+    if (length >= 2 && charAt(length - 2) == 13 && charAt(length - 1) == 10) {
       subSequence(0, length - 2)
-    else if (length >= 1 && (charAt(length - 1) == 13 || charAt(length - 1) == 10))
+    }
+    else if (length >= 1 && (charAt(length - 1) == 13 || charAt(length - 1) == 10)) {
       subSequence(0, length - 1)
+    }
     else this