diff options
| -rw-r--r-- | docs/ProgrammersManual.html | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/docs/ProgrammersManual.html b/docs/ProgrammersManual.html index b54441520a..a3b54f802b 100644 --- a/docs/ProgrammersManual.html +++ b/docs/ProgrammersManual.html @@ -407,7 +407,7 @@ program hasn't been started yet, you can always just run it with <!-- _______________________________________________________________________ --> <div class="doc_subsubsection"> - <a name="DEBUG_TYPE">Fine grained debug info with <tt>DEBUG_TYPE()</tt> and + <a name="DEBUG_TYPE">Fine grained debug info with <tt>DEBUG_TYPE</tt> and the <tt>-debug-only</tt> option</a> </div> |