tree 6e22091569b577e3d86132e60e53f14f7311b781
parent 4c90df33dab78d7895aa1121603d2680e7efefaf
author Dhruv Srivastava <dhruvsri@google.com> 1613586308 +0100
committer Dhruv Srivastava <dhruvsri@google.com> 1613650004 +0100

Move render only properties to RenderPreferences

Certain preferences cannot be changes by the users and are only
meant to determine the rendering of diff.
Move these properties to RenderPreferences.
Once other users of gr-diff have migrated, we can remove these
properties from DiffPreferencesInfo.

Change-Id: I80b92b8ae74877558321899f2426c36d244c12eb