--- 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