Extract docker in a standalone repository
Closes #3926 (closed)
Needs some more work on related parts:
- update jenkins jobs accordingly
- check/update the documentation
Docker directory has been extracted using a git subtree split -P <name-of-folder> -b <name-of-new-branch>
command to extract the history of the docker/ directory in a new branch, then pulling that branch in a fresh new docker git repo.
Edited by David Douard