[dack]

in a collaborative environment, it's rarely 30 seconds to make such a change though. usually you have to make a commit with message, make a PR, submit the PR and get someone to review it (many orgs require code review for every change), then merge it. And each of those steps usually require you to context switch from whatever else you were actually trying to get done.

Now, if you're already changing that part of the code/file, then sure it's pretty low overhead. But for something as simple as that function, I'd probably delete the comment entirely.

[whstl]

If something like that is generating a lot of bureaucracy and time-wasting, then there are several other pressing problems that are much worse than that.

My company is heavily regulated (finance) and highly bureaucratic, but I still just merge those PRs without waiting for the CI or without even bothering clicking approve, I just look at it. When I find one myself I just merge to master or edit in Github directly. No auditor has ever batted an eye to that.

[andelink]

For something as small as a code comment change, it's super fast, and honestly not worth the local branch stage -> commit -> push flow. Assuming GitHub, just edit it within the browser (if you find it in your editor, press the hotkey for opening the source in GitHub, if you're already in the browser, great). Make the change, hit commit (which defaults to a feature branch, you can change this), and then GitHub automatically opens up a PR template for your to then hit "create." Add reviewer(s), enable auto-merge, then forget about it.