diff options
Diffstat (limited to 'MANUAL.txt')
| -rw-r--r-- | MANUAL.txt | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/MANUAL.txt b/MANUAL.txt index 3e4425a72..29fde9168 100644 --- a/MANUAL.txt +++ b/MANUAL.txt @@ -733,10 +733,10 @@ Options affecting specific writers `--id-prefix=`*STRING* -: Specify a prefix to be added to all automatically generated identifiers - in HTML and DocBook output, and to footnote numbers in Markdown output. - This is useful for preventing duplicate identifiers when generating - fragments to be included in other pages. +: Specify a prefix to be added to all identifiers and internal links + in HTML and DocBook output, and to footnote numbers in Markdown + and Haddock output. This is useful for preventing duplicate + identifiers when generating fragments to be included in other pages. `-T` *STRING*, `--title-prefix=`*STRING* |