Re: [PATCH] doc: really get rid of Documentation/ directory