diff --git a/doc/dev/todo/steven b/doc/dev/todo/steven index 0383c23e..09c87851 100644 --- a/doc/dev/todo/steven +++ b/doc/dev/todo/steven @@ -5,7 +5,8 @@ Object: gencode_remote Type: - explorer_path + explorer_dir + remote_explorer_dir GlobalExplorer: out_path: local path into which the output is written