Is there any difference between Settings::devicePixelRatio [1] and
Settings::defaultDeviceScaleFactor [2] ? They appear to be used by
disjoint sets of ports. Shall we delete one in favor of the other?
Adam
[1] http://trac.webkit.org/browser/trunk/Source/WebCore/page/Settings.h#L478
[2] http://t
I don' t think devicePixelRatio() belongs in settings. It should be either be
obtained from the platform code in WebCore/WebKit, or pushed in via API.
Simon
On May 31, 2012, at 3:48 PM, Adam Barth wrote:
> Is there any difference between Settings::devicePixelRatio [1] and
> Settings::defaultDev
(top-posting to fit in)
Doesn't the same argument apply to *deviceScaleFactor? That doesn't make
sense as a Setting either.
Pushing one or both out of settings doesn't answer the question of whether
they are redundant. My gut feeling is that they are and we should fold
them together. Alternate
I agree, having this in Settings seems to imply that the browser's physical
device remains the same for its entire lifetime which is not true.
- Dana
On Thu, May 31, 2012 at 6:52 PM, James Robinson wrote:
> (top-posting to fit in)
>
> Doesn't the same argument apply to *deviceScaleFactor? That
I've been working on patches that remove target-densitydpi and/or
defaultDeviceScaleFactor, which is what caused me to ask this
question. I suspect they can both be removed, but I might need some
help from folks with development environments for the various ports
that use one or the other.
Adam
5 matches
Mail list logo
