| changeset 82778 | 803731b62180 |
| parent 82758 | 414ebfd5389b |
| child 82779 | ec6eb16e4692 |
--- a/src/Pure/Build/resources.scala Fri Jun 27 13:24:05 2025 +0200 +++ b/src/Pure/Build/resources.scala Fri Jun 27 13:37:36 2025 +0200 @@ -252,8 +252,6 @@ consolidate: List[Document.Node.Name]): Session.Change = Thy_Syntax.parse_change(resources, reparse_limit, previous, doc_blobs, edits, consolidate) - def commit(change: Session.Change): Unit = {} - /* theory and file dependencies */