diff options
Diffstat (limited to 'isar/interface')
| -rw-r--r-- | isar/interface | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/isar/interface b/isar/interface index 58f5a30c..21c2d83a 100644 --- a/isar/interface +++ b/isar/interface @@ -113,6 +113,8 @@ do [ -f "$FILE" ] && ARGS="$ARGS -l $FILE" done +[ -n "$XSYMBOL_INSTALLFONTS" ] && "$ISATOOL" installfonts -x + export PROOFGENERAL_ASSISTANTS=isar export PROOFGENERAL_LOGIC="$LOGIC" export PROOFGENERAL_XSYMBOL="$XSYMBOL" |