--- layout: fc_discuss_archives title: Message 3 from Frama-C-discuss on August 2019 ---
On Thu, Aug 15, 2019 at 7:35 PM Virgile Prevosto <virgile.prevosto at m4x.org> wrote: > > Indeed, there's only one way to change the fonts of the GUI: tweaking > $FRAMAC_SHARE/frama-c.rc. On linux, adding 14 or 16 to each font_name entry > in this file gives a result that looks big enough on a projector. > It works great! Thanks a million! The "solution" I found was ten times uglier: use a custom .gtkrc-2.0 file along the lines of https://ubuntuforums.org/showthread.php?t=846348 Now I shall give a great demo! Best, - Xavier Leroy > Best regards, > -- > E tutto per oggi, a la prossima volta > Virgile > _______________________________________________ > Frama-c-discuss mailing list > Frama-c-discuss at lists.gforge.inria.fr > https://lists.gforge.inria.fr/mailman/listinfo/frama-c-discuss -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20190816/b75acdf0/attachment.html>