- fixed Linux crashing (bug in SyncScroll optimization)
- *ugly patch* to fix ugly GUI font in Ubuntu.
Frankly, I would really like to know how to fix this font issue right. The problem is that we are now using "sans-serif" fontcofig alias as default GUI font, which is in Ububtu 606 defined as Dejavu Sans, which simply looks ugly and Gnome visibly does not use it as its font.
How I know how to read Ubuntu's font information, however it reads as "Sans 12". What I am not sure how to do is how to translate this "Sans" face-name to actual font used (which is apparently Bitstream Vera Sans).
Anyway, for the time being I fixed this issue by using Bistream Vera Sans as GUI font if available, "sans-serif" default if not.