Closed jordijoangimenez closed 3 months ago
@davidjwbbc Ok for you to merge to main
directly, or do you prefer to merge development
to main
without doing a release?
I think it's nicer for the git tree to bring the main and v1.2.x branches up to the same as development since these documentation changes are already present on that branch and the development branch is just that one documentation commit ahead of main and v1.2.x.
Thank you David. Good idea so we are consistent. Let me do
I've done it
Closing without merge of this PR as the same changes have been merged from the development branch.
This fixes sync with the development branch