github-actions/comment: Add PR write permission and use github.rest.* for rest API#2196

Merged

jvesely merged 1 commit intoPrincetonUniversity:develfrom jvesely:devel

Nov 10, 2021

+6-4

Commits on Nov 10, 2021

github-actions/comment: Add PR write permission and use github.rest.* for rest API
jvesely
committed