Closed turibe closed 4 months ago
Thx, I updated the PR (which just leaves some small fixes, can do a squash merge).
Yes, don't worry about multiple commits, I'll squash merge in the end.
Thanks!
Thanks for the fixes!
(oh, I used the PR title as the commit message, which is outdated. Oh well)
Thanks for the fixes!
(oh, I used the PR title as the commit message, which is outdated. Oh well)
Let's just say that I forgot the word "remove" in the PR title :-).
I see that I made a conflicting PR to this one which got merged: #467. That makes this PR mostly obsolete (and I don't think we should be linking to Lean Together events on this page). But you also fix some typos, so maybe update this PR or make a new one? Thanks