Closed rhuss closed 7 years ago
@rhuss I think you mistakenly pushed to a branch in the origin repo, just a heads up for next time please push to your fork (I know you know that, but just had to say it!).
Actually, I used the Github Web UI to edit and instead of committing it directly (which I do for smaller typos, shame on me), I went for a PR. I will delete the branch asap after the merge.
For documentation, I find it very convenient to fix it directly in the browser as the editor is quite matured these days. Unfortunately, my master branch is not really up-to-date all the time, so I took the lazy route (which hopefully is not that disturbing if I delete the branch. which I forget from time to time).
Ah yeah that is nice and easy.
Pull request approved by @jimmidyson - applying approved label
Done and branch deleted.
This seems to be the most popular installation variant these days.