
This change adds a font size field in diff preferences in both the generic preferences page and also the preferences modal from the diff view. The new field allows users to update their preferred font size for the diff view to be displayed. This updates both the line number font size as well as the diff font size. Feature: Issue 4417 Change-Id: I0fb75fd2186d2ff63b3627e8b0f15f2b3cddbfa3