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 /pygments/formatters/img.py | |
| parent | ce78dd107498f4b1bb53ee944f752578e2755109 (diff) | |
| download | pygments-21cd6ca55b236413f37e5679b7b6cd03ee928fea.tar.gz | |
Use the font_size option.
Diffstat (limited to 'pygments/formatters/img.py')
| -rw-r--r-- | pygments/formatters/img.py | 3 |
1 files changed, 2 insertions, 1 deletions
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') |