diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2008-07-12 14:00:46 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2008-07-12 14:00:46 +0000 |
| commit | 86d6f7053bba5cba50525f18e218a6784780b9e9 (patch) | |
| tree | 286fc11b54f563ce63eeccfb32833f03fd328187 /doc/PG-adapting.texi | |
| parent | 8b65a54fdeb50bc346fcf8d25315e54e28c4cca6 (diff) | |
Update docstrings
Diffstat (limited to 'doc/PG-adapting.texi')
| -rw-r--r-- | doc/PG-adapting.texi | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/PG-adapting.texi b/doc/PG-adapting.texi index c12a95c2..d7dc6fef 100644 --- a/doc/PG-adapting.texi +++ b/doc/PG-adapting.texi @@ -1529,7 +1529,7 @@ input, then newlines can be retained in the input. @c TEXI DOCSTRING MAGIC: proof-shell-insert-hook @defvar proof-shell-insert-hook -Hooks run by @code{proof-shell-insert} before inserting a command.@* +Hooks run by @samp{@code{proof-shell-insert}} before inserting a command.@* Can be used to configure the proof assistant to the interface in various ways -- for example, to observe or alter the commands sent to the prover, or to sneak in extra commands to configure the prover. |