diff options
Diffstat (limited to 'isar/interface')
| -rw-r--r-- | isar/interface | 10 |
1 files changed, 3 insertions, 7 deletions
diff --git a/isar/interface b/isar/interface index 6d61243b..a8821897 100644 --- a/isar/interface +++ b/isar/interface @@ -69,7 +69,7 @@ PROGNAME="xemacs" INITFILE="true" WINDOWSYSTEM="true" XSYMBOL="" -XSYMBOLSETUP=true +XSYMBOL_SETUP=true XSYMBOL_FONTSIZE="12" getoptions() @@ -89,7 +89,7 @@ getoptions() START_PG="$OPTARG" ;; X) - XSYMBOLSETUP="$OPTARG" + XSYMBOL_SETUP="$OPTARG" ;; f) XSYMBOL_FONTSIZE="$OPTARG" @@ -193,16 +193,12 @@ else [ "$INITFILE" = false ] && ARGS="$ARGS -q" if [ "$WINDOWSYSTEM" = true -a -n "$DISPLAY" ]; then - #ARGS="$ARGS -T Isabelle" - [ -n "$XSYMBOL_INSTALLFONTS" -a "$XSYMBOLSETUP" = true ] && installfonts + [ -n "$XSYMBOL_INSTALLFONTS" -a "$XSYMBOL_SETUP" = true ] && installfonts else ARGS="$ARGS -nw" XSYMBOL=false fi - [ ! "$XSYMBOLSETUP" = true ] && XSYMBOL_HOME="" - - ARGS="$ARGS -l '$SUPER/isa/interface-setup.el'" if [ -n "$KEYWORDS" ]; then |