src/Pure/Admin/other_isabelle.scala
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 */