more shell functions;
authorwenzelm
Sat, 24 Nov 2018 16:41:18 +0100
changeset 69342 fa981730b964
parent 69341 6aa24ccd8049
child 69343 395c4fb15ea2
more shell functions;
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 ()
 {