Commit Graph

1 Commits

Author SHA1 Message Date
Oliver Gugger
94183e0f52
docker+docs: move dev Dockerfile to root, document dev build
To finally end the discussion what Dockerfile should be used for what
and whether we should build from local source or check out from git, we
place both Dockerfiles next to each other and explicitly document their
purpose.
2020-11-23 14:48:45 +01:00