From c2db763cedc7ff4551c784235b215ac8e103f792 Mon Sep 17 00:00:00 2001
From: Makarius Wenzel
Date: Fri, 15 Sep 2000 15:06:39 +0000
Subject: isatool installfonts (for remote X-Symbol fonts);

---
 isa/interface  | 2 ++
 isar/interface | 2 ++
 2 files changed, 4 insertions(+)

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"
-- 
cgit v1.2.3