doc/Makedoc.sh: Do not preserve gzip timestamps when creating guide.ps.gz.

  This should make build a bit less unreproducible.
  Build timestamps are still present in pdf and dvi.
Signed-off-by: Agustin Martin Domingo's avatarAgustin Martin Domingo <[email protected]>
parent 04fab950
......@@ -139,7 +139,7 @@ for docformat in ${BUILDDOC_FORMATS}; do
fi
dvips -t ${DVIPS_PAPER} -o ./guide.ps ./guide.dvi
if [ -n "`which gzip`" -a -f ./guide.ps ]; then
gzip -fN ./guide.ps
gzip -fn ./guide.ps
fi
else
echo "- ++ Warning: dvips not available, cannot build \"guide.ps\"." >&2
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment