From 0bbb3d2b84a15d638e4381488b32d3bb7206a74b Mon Sep 17 00:00:00 2001
From: Makarius Wenzel
Date: Tue, 19 Sep 2000 21:57:55 +0000
Subject: installfonts only when using X window system;

---
 isar/interface | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

(limited to 'isar/interface')

diff --git a/isar/interface b/isar/interface
index 7f323fdf..8a6cfe48 100644
--- a/isar/interface
+++ b/isar/interface
@@ -117,6 +117,7 @@ ARGS=""
 
 if [ "$WINDOWSYSTEM" = true -a -n "$DISPLAY" ]; then
   ARGS="$ARGS -T Isabelle"
+  [ -n "$XSYMBOL_INSTALLFONTS" ] && "$ISATOOL" installfonts -x
 else
   ARGS="$ARGS -nw"
   XSYMBOL=false
@@ -131,8 +132,6 @@ do
   [ -f "$FILE" ] && ARGS="$ARGS -l $FILE"
 done
 
-[ -n "$XSYMBOL_INSTALLFONTS" ] && "$ISATOOL" installfonts -x
-
 export PROOFGENERAL_ASSISTANTS="$KIND"
 export PROOFGENERAL_LOGIC="$LOGIC"
 export PROOFGENERAL_XSYMBOL="$XSYMBOL"
-- 
cgit v1.2.3