On 10/02/2019 20:08, Peter Lammich wrote:
> No luck on my machine. The font rendering still looks slightly
> blurred.
>
> However, I'm using an old Linux (Ubuntu 16.04) ... may that be the
> reason?
I don't think so, but you can make a quick test by booting current
Ubuntu 18.04 from an USB stick. The graphics drivers could make a
difference.
Note that the jdk-11 distribution includes a copy of libfreetype.so, so
it appears to be reasonably self-contained in that respect. (I did not
read the relevant sources, because it is split between a Java and a
native part in C, and the latter sources always require extra work to
locate.)
Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
