0eb7e75421
Contribution now have to be made on the main branch. A new `documentation` branch is created. Github and Gitlab pipelines are now working on this branch. Develop branch is deprecated, as it is no more necessary.