changeset 68758 | a110e7e24e55 |
parent 68744 | 64fb127e33f7 |
child 68884 | 9b97d0b20d95 |
--- a/src/Pure/Tools/dump.scala Fri Aug 17 21:34:56 2018 +0200 +++ b/src/Pure/Tools/dump.scala Sat Aug 18 12:41:05 2018 +0200 @@ -17,7 +17,7 @@ deps: Sessions.Deps, output_dir: Path, node_name: Document.Node.Name, - node_status: Protocol.Node_Status, + node_status: Document_Status.Node_Status, snapshot: Document.Snapshot) { def write(file_name: Path, bytes: Bytes)