--- layout: fc_discuss_archives title: Message 3 from Frama-C-discuss on August 2019 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Changing fonts in frama-c-gui, MacOS



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>