Allow non-integer values in scaling options

[Player701]

Currently, in "Options -> HUD options -> Scaling options", it is only possible to set the scale sliders to integer values. It is not possible to set a value like 1.5, even via the console or by editing the INI file. On my new laptop with a 15.6 inch full HD screen, the default (unscaled) HUD feels too small, but if I set the scale to 2 (the next possible value after 1), it feels too big instead. It would be great if I could set it to something like 1.5 or 1.25.

[Graf Zahl]

These are pixel scaling factors. With values like 1.25 or 1.5 you'd get something very, very ugly if you did not use texture filtering to even out the differently sized texels.

[Player701]

Ouch. Didn't know that. Well, I actually do use texture filtering, but I guess there are people who don't, so it might not be possible to cater to everyone. Well, I definitely can live with 2x scaled HUD if that is the case.

[Graf Zahl]

Technically such values are no problem to implement. I just wanted to point out the caveat they might imply.

[Player701]

Well, maybe then some kind of warning should be issued if such values are used when texture filtering is not enabled. Or maybe they should not be allowed at all in the latter case. I'm no usability expert so I'm not sure what is best.

[Rachael]

What you can do is neighbor upscaling and then linear downscaling. That won't look too bad, but the non-HW2D backend won't support that.

[Graf Zahl]

I'm strictly against adding more cruft to handle edge cases.