github-actions[bot]
commented
6 months ago Your changes were successfully integrated in the dev site, make sure to review the pages of the projects you touched before merging this PR: https://holoviz-dev.github.io/examples/. You can also download an archive of the site from the workflow summary page which comes in handy when your dev site built was overriden by another PR (we have a single dev site!).
I previously set up permissions in the pr_flow workflow which propagate to the workflow it calls. When a PR is merged, the docs workflow runs on its own, it needs additional permissions to push to the repo. Note that setting one permission disables all the other ones (see https://docs.github.com/en/actions/using-jobs/assigning-permissions-to-jobs), so I had to explicitly allow writing to pull-requests too. Let's see!