On 6/26/23 13:37, Sean Fitzpatrick wrote:
> In the source for an HTML page, near the top, we have a comment that reads,
> "Generated from PreTeXt source". Would it make sense if we also added a line
> below giving the date on which the HTML was generated?
No, because then every diff I do will show changes on every single file
including sputious knowls. ;-)
BUT, peek inside "index.html"! A recent one of mine says:
*******************************************
* Generated from PreTeXt source
* on 2023-06-26T07:30:48-07:00
* A recent stable commit (2022-07-01):
* 6c761d3dba23af92cba35001c852aac04ae99a5f
*
*
https://pretextbook.org
*
*******************************************
Yes, anything that needs to be done on a regular basis grows cold eventually. ;-)
Automatically putting in a commit became a chicken-and-egg conundrum. You can
find something old on GitHub with some elaborate git wizardry.
You could volunteer to make a monthly PR to update the commit hash? Wouldn't be
too annoying on my end. ;- ;-) ;-)
Rob