tiny feature request: add meta date tag to HTML output

[Benno Schulenberg-3]

Hi,

When HTML pages produced by makeinfo are put online, it would be
nice if the reader could relatively easily find out when these pages
were produced.  This could be done by adding to the header after the
"generator" meta tag a "date" meta tag mentioning the then current
date.

For example:
<meta name="description" content="GNU Coreutils">
<meta name="generator" content="makeinfo 4.14">
<meta name="date" content="2009 september 11">

Benno

--
http://www.fastmail.fm - Does exactly what it says on the tin

[Karl Berry]

Hi Benno,

    "generator" meta tag a "date" meta tag mentioning the then current

I've thought about that, but then the pages are always changed on every
regeneration, even when nothing has actually changed.

On the other hand, thinking about again now, I realize that the
recommendation for GNU manuals is to include the date of last update in
the document itself, in the @copying block.  And therefore all the
generated pages are changed anyway.  And so adding the generation date
wouldn't actually be a problem.

Hmm.  Patrice, any opinion?

Thanks,
Karl

[Eli Zaretskii]

> Date: Sat, 19 Sep 2009 16:30:34 -0500
> From: karl@... (Karl Berry)
> Cc: bug-texinfo@...
>
> Hi Benno,
>
>     "generator" meta tag a "date" meta tag mentioning the then current
>
> I've thought about that, but then the pages are always changed on every
> regeneration, even when nothing has actually changed.
>
> On the other hand, thinking about again now, I realize that the
> recommendation for GNU manuals is to include the date of last update in
> the document itself, in the @copying block.  And therefore all the
> generated pages are changed anyway.  And so adding the generation date
> wouldn't actually be a problem.

Not every manual is a documentation of a GNU project, so not all of
them follow GNU standards.

So I think, if we adopt this as default, we should have an option to
turn it off.