chiark / gitweb /
docs: clear timestamp embedded in DVI comment field
authorReiner Herrmann <reiner@reiner-h.de>
Fri, 30 Oct 2015 18:27:18 +0000 (19:27 +0100)
committerReiner Herrmann <reiner@reiner-h.de>
Fri, 30 Oct 2015 18:27:18 +0000 (19:27 +0100)
docs/gendocs.sh

index a70b8e31167ca57d941d2b7af05b8d55cd28aec4..9e0bbb0cfade96725ca49ebe8efd24d1c112e6a9 100755 (executable)
@@ -46,7 +46,7 @@ templateurl="http://savannah.gnu.org/cgi-bin/viewcvs/~checkout~/texinfo/texinfo/
 
 : ${SETLANG="env LANG= LC_MESSAGES= LC_ALL= LANGUAGE="}
 : ${MAKEINFO="makeinfo"}
-: ${TEXI2DVI="texi2dvi -t @finalout"}
+: ${TEXI2DVI="TEX=\"tex -output-comment=''\" texi2dvi --output-comment=\"\" -t @finalout"}
 : ${DOCBOOK2HTML="docbook2html"}
 : ${DOCBOOK2PDF="docbook2pdf"}
 : ${DOCBOOK2TXT="docbook2txt"}