Hi,
I've just noticed that the date at the end of the
man page for gettimeofday(2) is "2017-09-15" in the most
current version from the git repository. But I also know
for sure that it was updated on 2018-05-13. That makes it
look as if that date is something that needs to be updated
manually which, of course, can easily be forgotten.
Perhaps that could be dealt with by a pre-commit hook.
Would there be any interest in me trying to come up with
something for this (in case my above assumption is
correct)?
Best regards, Jens
--
\ Jens Thoms Toerring ________ jt@xxxxxxxxxxx
\_______________________________ http://toerring.de
