diff --git a/doc/repl.md b/doc/repl.md index a31db4f..978bad2 100644 --- a/doc/repl.md +++ b/doc/repl.md @@ -39,7 +39,7 @@ See `Pantograph/Protocol.lean` for a description of the parameters and return va - `{ "goals": }`: Resume the given goals * `goal.remove {"stateIds": []}"`: Drop the goal states specified in the list * `goal.print {"stateId": }"`: Print a goal state -* `goal.save`{ id, path }, `env.load { path }`: Save/Load a goal state to/from a +* `goal.save{ id, path }`, `goal.load { path }`: Save/Load a goal state to/from a file. The environment is not carried with the state. The user is responsible to ensure the sender/receiver instances share the same environment. * `frontend.process { ["fileName": ",] ["file": ], invocations: