# HG changeset patch
# User wenzelm
# Date 1543074078 -3600
# Node ID fa981730b9645b36cc6411a6ec7b4f21606c2f28
# Parent  6aa24ccd8049ab0d306f8a00b08f50c8997bf7da
more shell functions;

diff -r 6aa24ccd8049 -r fa981730b964 lib/scripts/getfunctions
--- a/lib/scripts/getfunctions	Sat Nov 24 15:54:53 2018 +0100
+++ b/lib/scripts/getfunctions	Sat Nov 24 16:41:18 2018 +0100
@@ -125,6 +125,22 @@
 }
 export -f isabelle_scala_tools
 
+#Isabelle fonts
+function isabelle_fonts ()
+{
+  local X=""
+  for X in "$@"
+  do
+    if [ -z "$ISABELLE_FONTS" ]; then
+      ISABELLE_FONTS="$X"
+    else
+      ISABELLE_FONTS="$ISABELLE_FONTS:$X"
+    fi
+  done
+  export ISABELLE_FONTS
+}
+export -f isabelle_fonts
+
 #file formats
 function isabelle_file_format ()
 {