The docs building to be added to the CI contains at least two stages: doc_build and doc_deploy, where the documentation is built and deployed. The respective jobs should be triggered if PRs targeting main or dev are merged. Therefore, the deployment should be done for both, the development (i.e. latest) version lying on dev and the stable (i.e. released) version lying on main. The actual setup for this could be addressed in another issue.
The docs building to be added to the CI contains at least two stages:
doc_buildanddoc_deploy, where the documentation is built and deployed. The respective jobs should be triggered if PRs targetingmainordevare merged. Therefore, the deployment should be done for both, the development (i.e. latest) version lying ondevand the stable (i.e. released) version lying onmain. The actual setup for this could be addressed in another issue.