Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
4 changes: 2 additions & 2 deletions .CI/Jenkinsfile
Original file line number Diff line number Diff line change
Expand Up @@ -42,7 +42,7 @@ pipeline {
string(name: 'pull_request_baseline', defaultValue: 'master', description: 'The branch a pull request is compared against. Its newest run has to come from pull_request_node, or the report compares the machines as much as the pull request.')
string(name: 'pull_request_config', defaultValue: 'configs/conf.json', description: 'What a pull request run tests. A full run takes days, so a smaller configuration file is often the better question to ask.')
choice(name: 'pull_request_node', choices: ['ryzen-5950x-1', 'ryzen-5950x-2-1', 'ryzen-9950x'], description: 'The machine a pull request runs on. The default is the one that produces the master runs it is compared against.')
booleanParam(name: 'pull_request_comment', defaultValue: false, description: 'Post the summary of a pull request run as a comment on the pull request, replacing the one an earlier run posted. Needs a github-token credential; without it the report is still written and published, only not commented.')
booleanParam(name: 'pull_request_comment', defaultValue: false, description: 'Post the summary of a pull request run as a comment on the pull request, replacing the one an earlier run posted. Needs an OpenModelica-Hudson credential; without it the report is still written and published, only not commented.')
booleanParam(name: 'drop_stale_pull_request_tables', defaultValue: false, description: 'Drop the pr-<N> tables of pull requests that have been merged or closed, and of those tested more than 60 days ago. The reports published for them are not touched.')
}
environment {
Expand Down Expand Up @@ -644,7 +644,7 @@ pipeline {
def report = "./pr-report.py '${pullRequest()}' --baseline='${(params.pull_request_baseline ?: 'master').trim()}'"
if (params.pull_request_comment) {
// Whoever the token belongs to is who the comment comes from.
withCredentials([string(credentialsId: 'github-token', variable: 'GITHUB_TOKEN')]) {
withCredentials([string(credentialsId: 'OpenModelica-Hudson', variable: 'GITHUB_TOKEN')]) {
sh "${report} --comment"
}
} else {
Expand Down
6 changes: 3 additions & 3 deletions README.md
Original file line number Diff line number Diff line change
Expand Up @@ -372,9 +372,9 @@ reports.
adding to it when the same pull request is tested again. It posts as whoever the
token belongs to: `GITHUB_TOKEN` or `GH_TOKEN` in the environment, or the account
[`gh`](https://cli.github.com) is logged in as. In Jenkins it is the
`pull_request_comment` parameter, which takes the token from a `github-token`
credential; without one the report is still written and published, and the
summary is in the build log.
`pull_request_comment` parameter, which takes the token from an
`OpenModelica-Hudson` credential; without one the report is still written and
published, and the summary is in the build log.

Two things make a difference mean something other than "the pull request did
this", and the report says so when they apply: **the machine**, since two runs
Expand Down
Loading