diff options
| author | gbrandl <devnull@localhost> | 2008-09-07 19:37:59 +0200 |
|---|---|---|
| committer | gbrandl <devnull@localhost> | 2008-09-07 19:37:59 +0200 |
| commit | 21cd6ca55b236413f37e5679b7b6cd03ee928fea (patch) | |
| tree | 0d16a942bd3841a69ba05fafb5b53e112e2ded76 | |
| parent | ce78dd107498f4b1bb53ee944f752578e2755109 (diff) | |
| download | pygments-21cd6ca55b236413f37e5679b7b6cd03ee928fea.tar.gz | |
Use the font_size option.
| -rw-r--r-- | CHANGES | 7 | ||||
| -rw-r--r-- | pygments/formatters/img.py | 3 |
2 files changed, 9 insertions, 1 deletions
@@ -1,6 +1,13 @@ Pygments changelog ================== +Version 0.12 +------------ +(released XXX XX, 2008) + +- Actually use the `font_size` option of the image formatter. + + Version 0.11.1 -------------- (released Aug 24, 2008) diff --git a/pygments/formatters/img.py b/pygments/formatters/img.py index 0b5831b2..ec18480c 100644 --- a/pygments/formatters/img.py +++ b/pygments/formatters/img.py @@ -277,7 +277,8 @@ class ImageFormatter(Formatter): self.image_pad = get_int_opt(options, 'image_pad', 10) self.line_pad = get_int_opt(options, 'line_pad', 2) # The fonts - self.fonts = FontManager(options.get('font_name', '')) + fontsize = get_int_opt(options, 'font_size', 14) + self.fonts = FontManager(options.get('font_name', ''), fontsize) self.fontw, self.fonth = self.fonts.get_char_size() # Line number options self.line_number_fg = options.get('line_number_fg', '#886') |