diff --git a/mps/tool/github-ci-kick b/mps/tool/github-ci-kick index 63c7dce8981..8285693a9f0 100755 --- a/mps/tool/github-ci-kick +++ b/mps/tool/github-ci-kick @@ -30,7 +30,7 @@ # "Ravenbrook/mps" repository. # # 3. In "Permissions" expand "Repository permissions" and under -# "Actions" choose "Read-only". +# "Actions" choose "Read and write". # # NOTE: This script could use the GitHub CLI, but that would require # it to be installed by the user. @@ -66,7 +66,7 @@ test -z "${auth}" && usage curl --silent --show-error \ --request POST --data @- \ --header "Accept: application/vnd.github+json" \ - --header "Authorization: Bearer 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"\ + --header "Authorization: Bearer ${auth}"\ --header "X-GitHub-Api-Version: 2022-11-28" \ "https://api.github.com/repos/${org}/${repo}/actions/workflows/c-cpp.yml/dispatches" \ <<-EOF