changeset 69342 | fa981730b964 |
parent 69277 | 258bef08b31e |
child 69374 | ab66951166f3 |
--- 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 () {