This message was deleted.
# bug-reports
s
This message was deleted.
j
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
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
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
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
Got it. Thanks for the explanation, that's helpful.