diff --git a/README.md b/README.md index bfdea29..73444ac 100644 --- a/README.md +++ b/README.md @@ -110,6 +110,7 @@ The following settings govern the data that Coq will send to the server: - `Set Tactician Neural Metadata` adds text-based metadata to when communicating in graph-mode, such as hypothesis names, textual representation of proof states and textual representations of definition. This will slow down the communication protocol, and should only be enabled for debugging, or when otherwise needed. + To let Coq take care of starting and stopping the server, use the command ``` Set Tactician Neural Executable "external-server-executable --argument1 --argument2".