export BUILD_IN_DOCKER=1 to use Docker for building inside a Docker
container.
GDB debug file paths will be wrong after building inside the container,
use the script provided in `dist/gdbinit-docker` to set the correct GDB
substitution paths (copy and paste the contents into your `~/.gdbinit`)
The environment variable DOCKER_FLAGS can be used to pass extra
parameters to the Docker process.
