Join GitHub today
GitHub is home to over 31 million developers working together to host and review code, manage projects, and build software together.Sign up
Add search dialog #1101
This is a PR to add a View->Search popup box that searches the current name store for features that match a query. It uses both the "query" and "get" functions on the Name store so both those are considered a public interface.
This addresses #1081 and makes searching more accessible to users
Some design decision include