src/Pure/Tools/dump.scala
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)