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