GitLab

   as this is a document that belongs to the mysqldoc tree, it needs to
   be copied over manually (using the Bootstrap script), before doing an
   official release distribution. The file Docs/internals.texi in this tree
   is only a dummy file to keep "make dist" happy.