Every time something is merged without documenting it "because there is nothing in the manual at the moment" is another time the manual becomes more useless to users.

I was just asking, I can write something if desired. I just haven't found any place where I should put it and none of the items in the right-click menu in symbol tree is documented either right now. The searchbar in the plugin manager isn't documented either.

I'm not sure if documenting obvious things like filtering just doesn't add noise to the documentation without any real value.

—
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.