docs: add search pings information (!9074) · Merge requests · Administrator / sourcegraph · GitLab

Administrator requested to merge fa/search-ping-docs into master Mar 17, 2020

Created by: attfarhan

Follow-up from https://github.com/sourcegraph/sourcegraph/pull/8930. Adds details of new aggregated search metrics in pings to pings docs page.