If it were definitely a bug I would open an issue there, but since it’s an improvement that will probably only make a difference for a few people, I prefer not to comment anything on GitHub because they are probably already overloaded with improvement suggestions in other parts of the software.