author | wenzelm |
Sat, 15 Jun 2024 23:52:30 +0200 | |
changeset 80382 | 2740dec064f9 |
parent 80381 | 00600ebb8aa3 |
child 80383 | 224cdaaaf0cd |
--- a/src/Pure/General/bytes.scala Sat Jun 15 23:49:06 2024 +0200 +++ b/src/Pure/General/bytes.scala Sat Jun 15 23:52:30 2024 +0200 @@ -436,7 +436,7 @@ def proper: Option[Bytes] = if (is_empty) None else Some(this) - def +(other: Bytes): Bytes = + def + (other: Bytes): Bytes = if (other.is_empty) this else if (is_empty) other else {