Description of changes:
At some point in the past few months the documentation generation job stopped working due to permissions. This might be related to issues we had when we moved to the amazon-ion org, when org level permissions changed, I'm not sure though.
This PR adds content: write permissions to the document generation Job, so that we can push doc changes.
Github now supports publishing to github pages via actions, an alternative to pushing to gh-pages branch, which might be worth looking into in order to see pros/cons, it feels gross to allow write access to a repo via GHA.
By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 license.
Issue #, if available: N/A
Description of changes: At some point in the past few months the documentation generation job stopped working due to permissions. This might be related to issues we had when we moved to the amazon-ion org, when org level permissions changed, I'm not sure though.
This PR adds
content: writepermissions to the document generation Job, so that we can push doc changes.Github now supports publishing to github pages via actions, an alternative to pushing to gh-pages branch, which might be worth looking into in order to see pros/cons, it feels gross to allow write access to a repo via GHA.
By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 license.