The master branch is implemented using git subtrees (#2,#3,#10). The directories docs/, source/ and tools/ each track a dedicated branch on this repository. In this way it is possible to keep the documentation, source code and tools up to date on their dedicated branches, while the master branch reflects the last official release.
Unfortunately, the double nature of the docs as a directory on the master in addition to its own branch is a cause of confusion, with our contributors updating the documentation on the wrong location. In hindsight, implementing similar functionality with git submodules would have been simpler to set up and maintain.
Move to git submodules
[x] check that the docs/, source/ and tools/ sub directories on master have not diverged from their subtrees
Current situation with git subtrees
The
masterbranch is implemented using git subtrees (#2,#3,#10). The directoriesdocs/,source/andtools/each track a dedicated branch on this repository. In this way it is possible to keep the documentation, source code and tools up to date on their dedicated branches, while the master branch reflects the last official release.Unfortunately, the double nature of the
docsas a directory on themasterin addition to its own branch is a cause of confusion, with our contributors updating the documentation on the wrong location. In hindsight, implementing similar functionality with git submodules would have been simpler to set up and maintain.Move to git submodules
docs/,source/andtools/sub directories on master have not diverged from their subtrees