diff options
author | Makarius Wenzel <makarius@sketis.net> | 2000-09-15 15:06:39 +0000 |
---|---|---|
committer | Makarius Wenzel <makarius@sketis.net> | 2000-09-15 15:06:39 +0000 |
commit | c2db763cedc7ff4551c784235b215ac8e103f792 (patch) | |
tree | a943034df4d43673b58c3cf476cc785105ce22e1 | |
parent | 2837d07c6979ceafd197df3cc30b33d90c29e954 (diff) |
isatool installfonts (for remote X-Symbol fonts);
-rw-r--r-- | isa/interface | 2 | ||||
-rw-r--r-- | isar/interface | 2 |
2 files changed, 4 insertions, 0 deletions
diff --git a/isa/interface b/isa/interface index 3577fc39..64b66a08 100644 --- a/isa/interface +++ b/isa/interface @@ -113,6 +113,8 @@ do [ -f "$FILE" ] && ARGS="$ARGS -l $FILE" done +[ -n "$XSYMBOL_INSTALLFONTS" ] && "$ISATOOL" installfonts -x + export PROOFGENERAL_ASSISTANTS=isa export PROOFGENERAL_LOGIC="$LOGIC" export PROOFGENERAL_XSYMBOL="$XSYMBOL" 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" |