Except two minor remarks, this is great!

Where are those? Since I can't find them, maybe a minor remark of my own :-).

Sorry, I forgot to submit my review. Now done.

Maybe we should consider what widget in the sidebar gets the focus by default - right now it's the entry (and the tree focus is just one tab or enter press away) but maybe users who use primarily keyboard are more used to having the tree focused. I don't mind much myself as I just use mouse for the tree.

Same here and not sure what would be the best default.

I'd expected that it required more code to make the filter per document but happy to be proven wrong :D.

Same here and it actually applies to the whole patch. I was thinking about this feature for a long time but thinking it would be annoying to do and then saw the pull request which was pretty trivial and mostly working so I got attracted :-).

—
Reply to this email directly, view it on GitHub, or unsubscribe.
Triage notifications on the go with GitHub Mobile for iOS or Android.
You are receiving this because you are subscribed to this thread.