texi2dvi -o dir/file.dvi creates leftover file.dvi in pwd

[Ralf Wildenhues]

Hello Karl, bug-texinfo readers,

CVS texinfo has a bug over (well, that's what I had to compare with)
texinfo 4.8, in that
  texi2dvi -o dir/file.dvi ../source/dir/file.texi

sometimes (seemingly when tex is run several times) creates a leftover
file.dvi in the current directory.  This is annoying and causes
  make distcheck

failure in CVS Libtool, because $top_builddir/libtool.dvi is then a
leftover file after `make distclean'.

Glancing at the texi2dvi code and shell output, it seems that this
happens when the last tex command creates an identical dvi file, so
this branch:

      if cmp -s "$file" "$testdest"; then :; else
        verbose "Moving $file to $dest"
        mv "$file" "$dest"
      fi

is not executed, but also the original file is not removed.
Maybe that `then :' should instead be
      then rm -f "$file"

but I have no idea whether that can have negative consequences.  If you
need more information or would like me to look into the issue more then
please say so.

Oh, by the way, I also suffer from this annoying little info bug:
<http://lists.gnu.org/archive/html/bug-texinfo/2007-12/msg00029.html>

Thanks for maintaining texinfo.

Cheers,
Ralf