changeset 73340 | 0ffcad1f6130 |
parent 73136 | ca17e9ebfdf1 |
child 73357 | 31d4274f32de |
--- a/src/Pure/General/scan.scala Mon Mar 01 20:12:09 2021 +0100 +++ b/src/Pure/General/scan.scala Mon Mar 01 22:22:12 2021 +0100 @@ -478,7 +478,7 @@ def pos: InputPosition = new OffsetPosition(source, offset) def atEnd: Boolean = !seq.isDefinedAt(offset) override def drop(n: Int): Paged_Reader = new Paged_Reader(offset + n) - def close { buffered_stream.close } + def close: Unit = buffered_stream.close } new Paged_Reader(0) }