diff options
| author | Pierre-Marie Pédrot | 2020-01-13 16:24:15 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-01-14 13:55:46 +0100 |
| commit | 1e1aa9716e9bfac94fc6e50e428c304aa1bbec8f (patch) | |
| tree | d469e76e9dc2af8256fa98293c2ea2a75fdd326d /dev/include | |
| parent | 85f38599f59ada198260870aa64703348e739bd8 (diff) | |
Document the Set Default Proof Mode command.
Fixes #10909: Set Default Proof Mode is not documented.
Diffstat (limited to 'dev/include')
0 files changed, 0 insertions, 0 deletions