Git ignores .devcontainer
The files are already version controlled in the directory
`dev/.devcontainer`. Users would usually copy that directory into the
main repo directory and then modify it there. If there are changes to
be pushed upstream, they can always be applied into `dev/.devcontainer`.
