[PATCH 1/4] docker: Move 'docker' directory to 'tools'

[Stephen Finucane]

On 31 Aug 10:13, Daniel Axtens wrote:
> Somehow pressed 'r' instead of 'R' and failed to send this to the
> list, sorry!
> 
> The key bit:
> Acked-by: Daniel Axtens <dja at axtens.net>

Merged the v2 of this. Thanks for the review, Daniel.