| changeset 76666 | 981801179bc5 |
| parent 76663 | b7546c25e4f0 |
| child 76739 | cb72b5996520 |
--- a/src/Pure/PIDE/resources.scala Sat Dec 17 16:41:54 2022 +0100 +++ b/src/Pure/PIDE/resources.scala Sat Dec 17 17:02:09 2022 +0100 @@ -31,7 +31,6 @@ def sessions_structure: Sessions.Structure = session_background.sessions_structure def session_base: Sessions.Base = session_background.base - def session_errors: List[String] = session_background.errors override def toString: String = "Resources(" + session_base.print_body + ")"