diff options
| author | Ludovic Courtès <ludo@gnu.org> | 2019-07-15 12:33:07 +0200 |
|---|---|---|
| committer | Ludovic Courtès <ludo@gnu.org> | 2019-07-15 12:48:49 +0200 |
| commit | e591541d36215eda3aa2d877578e00939001fb85 (patch) | |
| tree | 658cca20ae70b1041620de1b10a8fe0484a30485 /gnu | |
| parent | 21bec78357ff5b93a14107bbeb5798923162f4b8 (diff) | |
| download | patches-e591541d36215eda3aa2d877578e00939001fb85.tar patches-e591541d36215eda3aa2d877578e00939001fb85.tar.gz | |
doc: Build a top-level index of the manuals.
Suggested by Julien Lepiller.
* doc/build.scm (html-manual-indexes)[build]: Add 'with-extensions'.
(translate): Actually honor DOMAIN. Add call to 'bindtextdomain' for
ISO-CODES.
(%iso639-languages): New variable.
(language-code->name, top-level-index): New procedures.
Add call to 'write-html' for OUTPUT/index.html.
Diffstat (limited to 'gnu')
0 files changed, 0 insertions, 0 deletions