Commit 565e64f9 authored by Samuel Hym's avatar Samuel Hym Committed by Manu Beffara
Browse files

Deduplicate *g:coq_debug* tag in help file

The tag *g:coq_debug* appeared twice so `helptags` did not know which
one should be the target
parent ce40b874
......@@ -233,10 +233,10 @@ The public Git repository of the project can be found at
https://git.framasoft.org/manu/coq-au-vim
*coq-debugging*
*coq-debugging* *g:coq_debug*
The Coq interaction plugin can be run in debugging mode by setting the
*g:coq_debug* variable. In this case, an extra window will be open on startup
and debugging messages will be appended there. The *g:coq_debug* variable is
|g:coq_debug| variable. In this case, an extra window will be open on startup
and debugging messages will be appended there. The |g:coq_debug| variable is
expected to be string, the presence of each letter below will trigger the
display of a particular kind of information:
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment