diff options
| -rw-r--r-- | otherlibs/graph/graphics.ml | 2 | ||||
| -rw-r--r-- | otherlibs/graph/text.c | 5 |
2 files changed, 6 insertions, 1 deletions
diff --git a/otherlibs/graph/graphics.ml b/otherlibs/graph/graphics.ml index d1cf5b9b2..27b3e9b4c 100644 --- a/otherlibs/graph/graphics.ml +++ b/otherlibs/graph/graphics.ml @@ -87,7 +87,7 @@ let fill_circle x y r = fill_arc x y r r 0 360 external draw_char : char -> unit = "gr_draw_char" external draw_string : string -> unit = "gr_draw_string" external set_font : string -> unit = "gr_set_font" -let set_text_size sz = () +external set_text_size : int -> unit = "gr_set_text_size" external text_size : string -> int * int = "gr_text_size" (* Images *) diff --git a/otherlibs/graph/text.c b/otherlibs/graph/text.c index 0e377964e..4076e22a8 100644 --- a/otherlibs/graph/text.c +++ b/otherlibs/graph/text.c @@ -34,6 +34,11 @@ value gr_set_font(value fontname) return Val_unit; } +value gr_set_text_size (value sz) +{ + return Val_unit; +} + static void gr_draw_text(char *txt, int len) { if (grfont == NULL) gr_font(DEFAULT_FONT); |