3 Commits (b82816c774ebdff076375fb5705b9f720ac9de67)

Author	SHA1	Message	Date
muxator	30fd53f1fd	docker: move docker/settings.json to /settings.json.docker	2019-11-08 23:50:50 +01:00
Pierre Prinetti	dc15f4a43c	docker: build from the local working directory ... With this change, the Dockerfile builds the Docker image from the code checked out in the local filesystem, instead of downloading a revision from git. Implements #3657	2019-11-08 22:56:30 +01:00
muxator	c008ee36bd	docker: incorporate the docker docs into the official documentation ... This also means increasing the indentation level.	2019-11-08 23:17:34 +01:00