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