Skip to content

Commit

Permalink
Fix
Browse files Browse the repository at this point in the history
  • Loading branch information
LasseBlaauwbroek committed Dec 24, 2023
1 parent 28c4d39 commit 31ce34c
Showing 1 changed file with 1 addition and 0 deletions.
1 change: 1 addition & 0 deletions README.md
Original file line number Diff line number Diff line change
Expand Up @@ -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".
Expand Down

0 comments on commit 31ce34c

Please sign in to comment.