Re: [basex-talk] Dpi scaling problem - Ubuntu 20.04

2020-10-18 Thread Christian Grün
Hi Silamphre, DPI scaling might be improved with a future version of Java (we only have limited means of improving rendering with Swing). With version of the JDK are you currently using / have you tried different versions? Best, Christian On Fri, Oct 16, 2020 at 4:12 AM Bridger Dyson-Smith wr

Re: [basex-talk] Dpi scaling problem - Ubuntu 20.04

2020-10-15 Thread Bridger Dyson-Smith
Hi Hugo - [responding to the list, too, because I'm well-known for missing the obvious! :)] On Thu, Oct 15, 2020 at 4:26 PM Silamphre wrote: > Hi Bridger, > > Thank you for your kind reply and your assistance. I have tried using that > command directly in the Ubuntu terminal, but unfortunately i

Re: [basex-talk] Dpi scaling problem - Ubuntu 20.04

2020-10-15 Thread Bridger Dyson-Smith
Hi Silamphre, I'm not sure if this will help or not, but editing the `basexgui` script to include `-Dsun.java2d.uiScale=1.25` might help[1]? I confess that I don't have UI scaling enabled on my unix-like system, or maybe you've already tried that approach. Hope that helps! Best, Bridger [1] https

[basex-talk] Dpi scaling problem - Ubuntu 20.04

2020-10-15 Thread Silamphre
Hello everyone, I started using BaseX for a class project a few days ago. I'd like to run it on my Ubuntu 20.04. I've installed openjdk version 14 to do so. I've set my Ubuntu display settings at 125% fractional scaling, but it appears that BaseX does not scale with this setting. The GUI conseque