changeset 69393 | ed0824ef337e |
parent 69365 | c5b3860d29ef |
child 69448 | 51e696887b81 |
--- a/src/Pure/General/bytes.scala Mon Dec 03 12:30:37 2018 +0100 +++ b/src/Pure/General/bytes.scala Mon Dec 03 14:59:42 2018 +0100 @@ -95,11 +95,8 @@ /* write */ - def write(file: JFile, bytes: Bytes) - { - val stream = new FileOutputStream(file) - try { bytes.write_stream(stream) } finally { stream.close } - } + def write(file: JFile, bytes: Bytes): Unit = + using(new FileOutputStream(file))(bytes.write_stream(_)) def write(path: Path, bytes: Bytes): Unit = write(path.file, bytes) }