Merge work.mysql.com:/home/bk/mysql-4.0/

into fred.bitbike.com:/home/arjen/mysql-4.0


Docs/manual.texi:
  Auto merged