changeset 73340 | 0ffcad1f6130 |
parent 71601 | 97ccf48c2f0c |
child 73359 | d8a0e996614b |
--- a/src/Pure/Admin/afp.scala Mon Mar 01 20:12:09 2021 +0100 +++ b/src/Pure/Admin/afp.scala Mon Mar 01 22:22:12 2021 +0100 @@ -90,7 +90,7 @@ val Extra_Line = """^\s+(.*)$""".r val Blank_Line = """^\s*$""".r - def flush() + def flush(): Unit = { if (section != "") result += (section -> props.reverse.filter(p => p._2.nonEmpty)) section = ""