Docs/manual.texi:
  removing lines that do not follow texi rules correctly.
  Hope Arjen can put this together properly ...