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