Backport and project card logic - #376
Conversation
| else if String.equal base_ref "refs/heads/master" then | ||
| (* For now, we hard code that PRs are only backported | ||
| from master. In the future, we could make this | ||
| configurable in the milestone description or in | ||
| some configuration file. *) |
There was a problem hiding this comment.
I guess this is going to be the opportunity to move this to the configuration file (can be in a followup PR).
There was a problem hiding this comment.
Since this call starts to be generic, I think the project_action function also needs to be made generic (currently, it still hardcodes Rocq in one place).
By the way, I believe that project_action was moved to bot-components/github/GitHub_automation.ml by mistake (in a previous PR) and it should probably appear in src/actions/ instead.
There was a problem hiding this comment.
I have moved the function project_action to src/action and fix the missing hardcode Rocq in this commit: be7b2af
Zimmi48
left a comment
Zimmi48
left a comment
There was a problem hiding this comment.
Nits to (optionally) address before merging.
| with | ||
| | None -> | ||
| Server.respond_string ~status:`OK | ||
| ~body:"Unsupported pull request card edition." () |
There was a problem hiding this comment.
I suggest making the message a little different from the standard case, because here it looks like a backporting project, but we just don't have the project configured.
| Server.respond_string ~status:`OK | ||
| ~body:"Unsupported pull request card edition." () | ||
| | Some repo_config -> | ||
| let backport_to = String.drop_suffix field 7 in |
There was a problem hiding this comment.
In passing: we drop a 7-character suffix because we expect the field to be called <branchname> status, which we checked above. This might be worth detailing in a comment here, and (later) in documentation.
2 participants
rocq_push_actiontopush_actionand drive owner/repo/project/org fromrepo_configadd_to_columnwith organization and project numbergithub_project_numberis absent; matchPullRequestCardEditedvia install id + project number from configgithub_project_numberRemaining Rocq hardcodes for follow-up PRs.