diff --git a/doc/dev/todo/steven b/doc/dev/todo/steven index b79b719b..35648910 100644 --- a/doc/dev/todo/steven +++ b/doc/dev/todo/steven @@ -7,6 +7,8 @@ Object: Type: type.transferred_explorers + type.type_explorer_paths() -> relative list of paths of explorer + GlobalExplorer: out_path: local path into which the output is written