Did this happen today (just now)? You can DM me the pr repo/# to confirm, but if it was today, it looks like you selected "merge" as a strategy and the repo doesn't allow merge commits.
🙏 1
b
Ben Hefner
05/18/2023, 6:37 PM
Yeah, looks like you're right. I haven't ever paid much attention to the merge strategy before - does that get defaulted when the PR is created perhaps? I just changed the rules on this particular repo today, after creating the PRs but before attempting to land them.
j
Jacob Gold
05/18/2023, 6:42 PM
github's api does actually vend us a default option that should match whatever you last used in that repo, but it's slow to update + also doesn't respect repo settings much of the time. we can do better here, namely checking the repo rules and overriding their default if necessary
Jacob Gold
05/18/2023, 6:43 PM
the default is per person per repo, not per pr, it's just not reliable -- e.g. we've noticed that whenever a new eng starts at our company their default shows up as merge as well (we also disallow merge commits)
b
Ben Hefner
05/18/2023, 6:43 PM
Got it. Thanks for the explanation, that's helpful.