aboutsummaryrefslogtreecommitdiff
path: root/ide/wg_ScriptView.ml
diff options
context:
space:
mode:
authorHugo Herbelin2019-02-07 16:54:11 +0100
committerVincent Laporte2019-03-19 08:40:21 +0000
commit4d69a22ffa06005b11040c9db9064a1d730eeb7f (patch)
tree548a617e30615d1464ce5094d0f6ea0ccf87f98c /ide/wg_ScriptView.ml
parent73847d367b22b5d451bcf1e538b80ca057232754 (diff)
Fix for post-beta3 lablgtk3 changes about cairo (from Claudio).
Diffstat (limited to 'ide/wg_ScriptView.ml')
-rw-r--r--ide/wg_ScriptView.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/ide/wg_ScriptView.ml b/ide/wg_ScriptView.ml
index 7812f1a222..e95176bf4d 100644
--- a/ide/wg_ScriptView.ml
+++ b/ide/wg_ScriptView.ml
@@ -484,7 +484,7 @@ object (self)
stick tab_length self self#set_tab_width;
stick auto_complete self self#set_auto_complete;
- let cb ft = self#misc#modify_font (Pango.Font.from_string ft) in
+ let cb ft = self#misc#modify_font (GPango.font_description_from_string ft) in
stick text_font self cb;
()