Monoid update: the boring parts#154
Conversation
MatthijsBlom
requested review from
konsumlamm,
memowe,
pierluc-codes,
smith558,
ulysses4ever and
xogcox
as code owners
|
We currently try to avoid merge commits, so your branch isn't mergeable right now. Can you fix it? I'm sorry for the extra trouble... |
|
I thought I fixed the conflicts in 58651fd. The web UI says there are no conflicts. Did something go wrong? |
|
You updated the branch from the GitHub UI (I assume) which created a merge commit, and we currently have a branch protection rule against merge commits... If I were you, I'd check out the branch locally, reset hard to the commit previous to the merge commit, rebased on main, and force-pushed. |
|
If it sounds too complicated, I can do it a bit later today actually |
|
Great, I take it that note isn't shown to non-maintainers: 
Do you prefer a single squashed commit, or two fast-forwardable commits? |
|
two commits are fine since eacch has a clear purpose on its own |
MatthijsBlom
force-pushed
the
monoid-update-boring-parts
branch
from
58651fd to
e3332a6
Compare
|
Merged! Thank you and sorry again for the git history trouble. |
2 participants
Sub-PR of #146, because GH's UI is not suited to reviewing individual commits.