tuned;
authorwenzelm
Sun, 26 Mar 2023 15:02:08 +0200
changeset 77714 be0b9396604e
parent 77713 0d6e592d24c0
child 77715 27dd3a3fcc54
tuned;
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