doc(export): add link to note

[robstoll]

No description provided.

[smarter]

Your PRs are very much appreciated, but could you try batching your documentation changes in fewer PRs ? It's easier to review and it strains our CI less.

[robstoll]

The thing is, I usually do those PRs when I am using the public transport system where I have a few minutes and never know if I can finish something or not. I am creating those from my phone and hence it is easier for me to create small PRs but I understand that your concern. So far I tried to do one PR per file which is easy enough as I can simply click on edit file and do the changes. Changing another file in the same PR is already more cumbersome for me. How about the following compromise:

• I create several branches, one per file
• I merge those branches into one branch and create then a PR
• you can still squash the commits during merge

Would that be a suitable way for you?

Regarding CI, IMO we should improve there and not improve on the contributor side. I hope your CI is able to set triggers for jobs and base them on changes in the commit. This way it would be easy to disable all the jobs which are not checking the docs in case changes are only in /docs/...
I can try to help out if required

[smarter]

Would that be a suitable way for you?

Sure!