diff --git a/doc/dev/todo/steven b/doc/dev/todo/steven index 77b74451..41306a66 100644 --- a/doc/dev/todo/steven +++ b/doc/dev/todo/steven @@ -10,6 +10,9 @@ Type: explorer_dir remote_explorer_dir + explorer_remote_dir + + GlobalExplorer: out_path: local path into which the output is written