2 Commits (0a86024797ed4d314133e33efbe1a4bfcbcb2128)

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