diff options
| author | Ludovic Courtès <ludo@gnu.org> | 2022-01-18 22:20:12 +0100 |
|---|---|---|
| committer | Ludovic Courtès <ludo@gnu.org> | 2022-01-18 22:51:08 +0100 |
| commit | 7eb883b7c284c78cc17093bfc4ef2d70e0acad83 (patch) | |
| tree | d6cb9d8b7879da6af715b03e5185584965e795d9 /gnu | |
| parent | ee16e4e8dac9fd14340cd96731e867134cd843fe (diff) | |
doc: Add a language menu in the HTML manual.
* doc/build.scm (stylized-html): New procedure.
(html-manual): Use it.
Diffstat (limited to 'gnu')
0 files changed, 0 insertions, 0 deletions