src/Pure/General/graphics_file.scala
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