GitLab

  references to the .texi file and the build targets that depend on manual.texi as the input file.
- added COPYING as a regular file instead of creating it during the build. This ensures that it's part
  of the sources when pulling from BK (it used to be extracted from the manual)
- Removed a lot of cruft and unused/obsolete stuff from the Docs directory (e.g. Flags, Images)
- added a dummy mysql.info placeholder file (the info file is still used as the source to extract
  various text files during the build). It will be replaced with a "real" file during the Bootstrap
  process to create the official source distribution - the placeholder just satisfies build dependencies.


BitKeeper/deleted/.del-manual.texi~af95f3e233925495:
  Delete: Docs/manual.texi
BitKeeper/deleted/.del-manual_toc.html~f483f2d33d9acb41:
  Delete: Docs/manual_toc.html
BitKeeper/deleted/.del-manual.de.texi~68483e0cb1187601:
  Delete: Docs/ma...