diff options
| -rwxr-xr-x | Master/tlpkg/bin/tl-update-auto | 14 |
1 files changed, 12 insertions, 2 deletions
diff --git a/Master/tlpkg/bin/tl-update-auto b/Master/tlpkg/bin/tl-update-auto index 1293f489053..a46b0bb1283 100755 --- a/Master/tlpkg/bin/tl-update-auto +++ b/Master/tlpkg/bin/tl-update-auto @@ -141,11 +141,21 @@ for gnuconf in config.guess config.sub; do done -# tlmgr man page autogenerated. +# tlmgr man page autogenerated. Don't worry about a date difference. # +# return 0 if files $1 and $2 are the same except for the first lines. +# (we need to ignore the timestamps in the generation lines.) +same_except_for_th () +{ + rm -f /tmp/seft1 /tmp/seft2 + sed '/^\.TH/d' <"$1" >/tmp/seft1 + sed '/^\.TH/d' <"$2" >/tmp/seft2 + cmp -s /tmp/seft1 /tmp/seft2 +} + manfile=texmf/doc/man/man1/tlmgr.1 pod2man bin/i386-linux/tlmgr >$temp -if $diff $manfile $temp >$temp.tlmgr.diff; then +if same_except_for_th $manfile $temp; then echo " `basename $manfile` ok." rm -f $manfile.new else |