doc: fix typos/indentation #3085
Conversation
marcusrossel
requested review from
kim-em,
leodemoura and
Kha
as code owners
|
Thanks for your contribution! I'm not sure how useful indentation fixes are when you aren't already touching the code (if it causes a merge conflict for someone else probably not), so don't go out of your way to fix them, but typo fixes are certainly appreciated. |
github-actions
bot
added
the
toolchain-available
|
@nomeata Are these kinds of small chore-PRs generally welcome, or are they more noise than they're worth? |
|
That is a good question. I’d say anything user-visible and obviously annoying (typos, wrong references in docstrings) is very welcome. Fixes to user-visible markup (bold theorem name) maybe as well, if it improves consistency. Typos in comments when they annoy you, but not need to be proactive about them. Indentation changes I personally don’t care too much about and would leave it to whoever touches the code next. If you expect to do more, then grouping multiple similar ones in one PR makes reviewing quicker. |
Head branch was pushed to by a user without write access
|
(Sorry, that last commit was by accident, but I guess it's also enough of a chore that I'll just leave it in.) |
|
Ok, now I'm confused how the PR even got merged, but does not include the final commit... |
leanprover-community-mathlib4-bot
added
the
builds-mathlib
|
|
Maybe there was a race condition with the Github merge queue. But separate PR is better anyways, since it isn’t about |
No description provided.