diff options
| author | Ludovic Courtès <ludo@gnu.org> | 2020-10-19 13:21:26 +0200 |
|---|---|---|
| committer | Ludovic Courtès <ludo@gnu.org> | 2020-10-19 13:28:38 +0200 |
| commit | d66a4eac4402614a1938fdc4ef0fde0c06badb52 (patch) | |
| tree | 1a43465b83c11f6b9ed0f26e4e762bc9ca2c312b /gnu | |
| parent | a9105c2c4c97ffbdb1b09dadc14773566924ab59 (diff) | |
doc: Produce stylable HTML for @deftp, @deffn, etc.
'makeinfo --help' uses <strong> and <em> for those entries. Replace
that with CSS classes.
* doc/build.scm (html-manual-identifier-index)[build]: Adjust to handle
rewritten forms of <dt> entries.
* doc/build.scm (syntax-highlighted-html)[build][syntax-highlight]:
Handle <dt> forms and replace them.
[highlight-definition, space?]: New procedures.
Diffstat (limited to 'gnu')
0 files changed, 0 insertions, 0 deletions