Address interactive search PR comments (!7242) · Merge requests · Administrator / sourcegraph · GitLab

Administrator requested to merge fa/pr-follow-up into master Dec 17, 2019

Created by: attfarhan

Addresses remaining comments in https://github.com/sourcegraph/sourcegraph/pull/7168