# HG changeset patch
# User wenzelm
# Date 1543500438 -3600
# Node ID 2c0af1c2e7235f706f4c057079f8c331205c0538
# Parent  69de0f5618247a97d9532d9b8c963ff81422c462
generate full component;

diff -r 69de0f561824 -r 2c0af1c2e723 Admin/isabelle_fonts/README
--- a/Admin/isabelle_fonts/README	Thu Nov 29 14:43:11 2018 +0100
+++ b/Admin/isabelle_fonts/README	Thu Nov 29 15:07:18 2018 +0100
@@ -17,7 +17,7 @@
 
 
     Makarius
-    23-Nov-2018
+    29-Nov-2018
 
 
 ----------------------------------------------------------------------------
diff -r 69de0f561824 -r 2c0af1c2e723 src/Pure/Admin/build_fonts.scala
--- a/src/Pure/Admin/build_fonts.scala	Thu Nov 29 14:43:11 2018 +0100
+++ b/src/Pure/Admin/build_fonts.scala	Thu Nov 29 15:07:18 2018 +0100
@@ -264,6 +264,29 @@
           Fontforge.close)
       ).check
     }
+
+
+    // etc/settings
+
+    val settings_path = target_dir + Path.explode("etc/settings")
+    Isabelle_System.mkdirs(settings_path.dir)
+    File.write(settings_path,
+      "# -*- shell-script -*- :mode=shellscript:\n\nisabelle_fonts \\\n" +
+      (for ((path, _) <- targets)
+        yield """  "$COMPONENT/""" + path.file_name + "\"").mkString(" \\\n") +
+      """
+
+if [ -z "$ISABELLE_FONTS_HTML" ]
+then
+  ISABELLE_FONTS_HTML="$COMPONENT/Vacuous.ttf"
+else
+  ISABELLE_FONTS_HTML="$ISABELLE_FONTS_HTML:$COMPONENT/Vacuous.ttf"
+fi
+""")
+
+
+    // README
+    File.copy(Path.explode("~~/Admin/isabelle_fonts/README"), target_dir)
   }