--- a/src/Pure/Admin/other_isabelle.scala Wed Nov 28 13:59:29 2018 +0100
+++ b/src/Pure/Admin/other_isabelle.scala Wed Nov 28 14:00:22 2018 +0100
@@ -61,8 +61,9 @@
val etc_settings: Path = etc + Path.explode("settings")
val etc_preferences: Path = etc + Path.explode("preferences")
- def fonts(html: Boolean = false): List[Path] =
- Isabelle_Fonts.files(html = html, getenv = getenv(_))
+ def copy_fonts(target_dir: Path): Unit =
+ Isabelle_Fonts.make_entries(getenv = getenv(_), html = true).
+ foreach(entry => File.copy(entry.path, target_dir))
/* settings */