| changeset 65589 | f70c617e9c26 |
| parent 64934 | 795055a0be98 |
| child 66232 | be0ab4b94c62 |
| 65588:b0d8d97198b3 | 65589:f70c617e9c26 |
|---|---|
152 } |
152 } |
153 |
153 |
154 |
154 |
155 /* read */ |
155 /* read */ |
156 |
156 |
157 def read(file: JFile): String = Bytes.read(file).toString |
157 def read(file: JFile): String = Bytes.read(file).text |
158 def read(path: Path): String = read(path.file) |
158 def read(path: Path): String = read(path.file) |
159 |
159 |
160 |
160 |
161 def read_stream(reader: BufferedReader): String = |
161 def read_stream(reader: BufferedReader): String = |
162 { |
162 { |