Skip to content

Fix zizmor's excessive permissions and fix deployment of docs - #550

Merged
santisoler merged 5 commits into
mainfrom
fix-docs-deployment
Apr 1, 2025
Merged

Fix zizmor's excessive permissions and fix deployment of docs#550
santisoler merged 5 commits into
mainfrom
fix-docs-deployment

Conversation

@santisoler

@santisoler santisoler commented Feb 11, 2025

Copy link
Copy Markdown
Member

Explicitly set permissions in GitHub Actions to solve zizmor's excessive-permissions errors. Fix deployment of docs by preserving credentials after checking out the gh-pages branch: we need those credentials to push to that branch. Use set -e in deployment script.

Relevant issues/PRs:

Inspired by fatiando/choclo#119 and fatiando/choclo#122.

Related to fatiando/community#166

Preserve credentials after checking out the `gh-pages` branch: we need
those credentials to push to that branch.
Solve zizmor's `excessive-permissions` errors.
@santisoler santisoler changed the title Fix deployment of docs by preserving credentials Fix zizmor's excessive permissions and fix deployment of docs Feb 11, 2025
@santisoler
santisoler marked this pull request as ready for review February 18, 2025 23:07
@leouieda

leouieda commented Apr 1, 2025

Copy link
Copy Markdown
Member

Did the segfault magically disappear?

@santisoler
santisoler merged commit 10a58ce into main Apr 1, 2025
@santisoler
santisoler deleted the fix-docs-deployment branch April 1, 2025 18:27
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants