Closed Tectu closed 2 years ago
Thanks for the fix! I will merge it soon.
Closing != Merging :p
I prefer not to create merge commits for the single commit branches as they seem useless to me and GitHub doesn't provide any way to mark a PR as "merged" if it was cherry-picked from outside the web UI (which I'd rather not use if possible), so, unfortunately, we have to live with this side effect. I don't think it makes any difference in practice, does it?
I don't think it makes any difference in practice, does it?
Nah, I was just wondering whether you maybe accidentally hit the "comment & close" button which might lead to this PR being forgotten about as it wouldn't show up as an open/active PR anymore :D
Fix a minor typo in
docs/types.md