Oh, I've just noticed the difference between the two ! Sorry for my previous comment and thanks for the clarification. That's a nice feature addition indeed.

I'm so use to the search mode only that I think I would prefer to keep the tree focused, but I would understand that someone else think the other way, in which case the correction suggested by @ntrel is surely better than mine (shorter and more readable).

—
Reply to this email directly, view it on GitHub, or unsubscribe.
You are receiving this because you are subscribed to this thread.