changeset 73340 | 0ffcad1f6130 |
parent 66114 | c137a9f038a6 |
child 75393 | 87ebf5a50283 |
--- a/src/Pure/PIDE/text.scala Mon Mar 01 20:12:09 2021 +0100 +++ b/src/Pure/PIDE/text.scala Mon Mar 01 22:22:12 2021 +0100 @@ -92,7 +92,7 @@ { val result = new mutable.ListBuffer[Range] var last: Option[Range] = None - def ship(next: Option[Range]) { result ++= last; last = next } + def ship(next: Option[Range]): Unit = { result ++= last; last = next } for (range <- ranges.sortBy(_.start)) {