changeset 72376 | 04bce3478688 |
parent 72375 | e48d93811ed7 |
child 72763 | 3cc73d00553c |
--- a/src/Pure/Admin/build_fonts.scala Mon Oct 05 21:15:58 2020 +0200 +++ b/src/Pure/Admin/build_fonts.scala Mon Oct 05 22:07:25 2020 +0200 @@ -307,8 +307,7 @@ // etc/settings - val settings_path = Components.settings(target_dir) - Isabelle_System.make_directory(settings_path.dir) + val settings_path = Isabelle_System.make_directory(Components.settings(target_dir)) def fonts_settings(hinted: Boolean): String = "\n isabelle_fonts \\\n" +