changeset 76661 | 0c7c6fa71ac3 |
parent 76657 | a8d85b4a588c |
child 76663 | b7546c25e4f0 |
--- a/src/Pure/PIDE/resources.scala Sat Dec 17 10:18:12 2022 +0100 +++ b/src/Pure/PIDE/resources.scala Sat Dec 17 11:25:10 2022 +0100 @@ -33,7 +33,7 @@ def session_base: Sessions.Base = session_background.base def session_errors: List[String] = session_background.errors - override def toString: String = "Resources(" + session_base.toString + ")" + override def toString: String = "Resources(" + session_base.print_body + ")" /* init session */