changeset 73317 | df49ca5da9d0 |
parent 73243 | 7f55a3e28c88 |
child 73340 | 0ffcad1f6130 |
--- a/src/Pure/Admin/other_isabelle.scala Sat Feb 27 17:33:40 2021 +0100 +++ b/src/Pure/Admin/other_isabelle.scala Sat Feb 27 18:04:29 2021 +0100 @@ -65,7 +65,7 @@ def copy_fonts(target_dir: Path): Unit = Isabelle_Fonts.make_entries(getenv = getenv, hidden = true). - foreach(entry => File.copy(entry.path, target_dir)) + foreach(entry => Isabelle_System.copy_file(entry.path, target_dir)) /* components */