diff options
| author | Karl Berry <karl@freefriends.org> | 2012-08-25 08:39:03 -0700 |
|---|---|---|
| committer | Karl Berry <karl@freefriends.org> | 2012-08-25 08:39:03 -0700 |
| commit | f7984c755853f26d42fe7f8905622c4c61dbe10e (patch) | |
| tree | 30aced7051df597ac9586759bc86644c40cd0758 /doc | |
| parent | e8ffd3e331423a5202faa58a5175d35c6ba42b58 (diff) | |
| download | gnulib-f7984c755853f26d42fe7f8905622c4c61dbe10e.tar.gz | |
autoupdate
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/maintain.texi | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/doc/maintain.texi b/doc/maintain.texi index aab6cdcb2e..9549192f94 100644 --- a/doc/maintain.texi +++ b/doc/maintain.texi @@ -5,7 +5,7 @@ @c For double-sided printing, uncomment: @c @setchapternewpage odd @c This date is automagically updated when you save this file: -@set lastupdate June 12, 2012 +@set lastupdate August 24, 2012 @c %**end of header @dircategory GNU organization @@ -2056,9 +2056,9 @@ gendocs.sh --email bug-texinfo@@gnu.org -o info info "GNU Info manual" gendocs.sh --email bug-texinfo@@gnu.org -o info-stnd info-stnd "GNU info-stnd manual" @end smallexample -By default, the script uses @command{makeinfo} for generating -@acronym{HTML} output. If you prefer to use @command{texi2html}, use -the @option{--texi2html} command line option, e.g.: +By default, the script uses @command{makeinfo} for generating HTML +output. If you prefer to use @command{texi2html}, use the +@option{--texi2html} command line option, e.g.: @smallexample gendocs --texi2html -o texinfo texinfo "GNU Texinfo manual" |