Frama-C-discuss mailing list archives
This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[Frama-c-discuss] Changing fonts in frama-c-gui, MacOS
- Subject: [Frama-c-discuss] Changing fonts in frama-c-gui, MacOS
- From: xavier.leroy at college-de-france.fr (Xavier Leroy)
- Date: Fri, 16 Aug 2019 10:39:52 +0200
- In-reply-to: <CA+yPOVixuUhnpLTJph4uxvyP0JkUXwR9tqrQxgZeg_cOHBJjEQ@mail.gmail.com>
- References: <CAH=h3gHQT+dG3p1ZC0CBgcExT9kaJgu=Gktx8Pb=mOdfNLq_5A@mail.gmail.com> <CA+yPOVixuUhnpLTJph4uxvyP0JkUXwR9tqrQxgZeg_cOHBJjEQ@mail.gmail.com>
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>
- References:
- [Frama-c-discuss] Changing fonts in frama-c-gui, MacOS
- From: xavier.leroy at college-de-france.fr (Xavier Leroy)
- [Frama-c-discuss] Changing fonts in frama-c-gui, MacOS
- From: virgile.prevosto at m4x.org (Virgile Prevosto)
- [Frama-c-discuss] Changing fonts in frama-c-gui, MacOS
- Prev by Date: [Frama-c-discuss] Changing fonts in frama-c-gui, MacOS
- Next by Date: [Frama-c-discuss] Struct with flexible array member within union
- Previous by thread: [Frama-c-discuss] Changing fonts in frama-c-gui, MacOS
- Next by thread: [Frama-c-discuss] Struct with flexible array member within union
- Index(es):