changeset 80368 | 9db395953106 |
parent 75394 | 42267c650205 |
--- a/src/Pure/General/graphics_file.scala Sat Jun 15 17:16:14 2024 +0200 +++ b/src/Pure/General/graphics_file.scala Sat Jun 15 20:14:24 2024 +0200 @@ -51,7 +51,7 @@ val params = new DefaultFontMapper.BaseFontParameters(File.platform_path(entry.path)) params.encoding = BaseFont.IDENTITY_H params.embedded = true - params.ttfAfm = entry.bytes.array + params.ttfAfm = entry.bytes.make_array mapper.putName(entry.name, params) } mapper