changeset 73425 | d0f529d5c5c9 |
parent 73422 | fc7a0ea94c43 |
child 73429 | 8970081c6500 |
--- a/src/Pure/General/http.scala Sat Mar 13 14:27:34 2021 +0100 +++ b/src/Pure/General/http.scala Sat Mar 13 14:55:27 2021 +0100 @@ -30,6 +30,7 @@ encoding: String = default_encoding) { def text: String = new String(bytes.array, encoding) + def text_lines: List[String] = Library.trim_split_lines(text) } def read_content(file: JFile): Content =