Finally, I think we should not forget that the modification time of the .texi file impacts the modification date that is printed in the final output of the manual. Setting it to 1970 is awkward in this case.
Top-level
Finally, I think we should not forget that the modification time of the .texi file impacts the modification date that is printed in the final output of the manual. Setting it to 1970 is awkward in this case. 3 comments
@jas4711 @civodul Another option I considered to avoid the dependency on git is to have another syntax-check that would check that you also changed the modification date of the manual in the most recent commit that modified it. It’s harmless to skip this check if you have a shallow clone of the repository or not have git installed. |
@gugurumbe @civodul Having modtime influence PDF output seems bad - can’t we use a @DATE@ macro set at ./configure-time that the .texi file @include? It should probably the time of the last commit to the project.