diff options
| author |  Makarius Wenzel <makarius@sketis.net> | 2005-07-19 16:24:26 +0000 |
|---|---|---|
| committer | Makarius Wenzel <makarius@sketis.net> | 2005-07-19 16:24:26 +0000 |
| commit | fc1c3f61737da67ff63532d5c201d16e455e8af2 (patch) | |
| tree | 757762b6b37059568c71a0eb467aa97499d38ca4 /isa | |
| parent | c31e2507bb0580b71be737106ee46b994dd8fbd6 (diff) | |
tuned;
Diffstat (limited to 'isa')
| -rw-r--r-- | isa/interface | 10 |
1 files changed, 3 insertions, 7 deletions
diff --git a/isa/interface b/isa/interface index 6d61243b..a8821897 100644 --- a/isa/interface +++ b/isa/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 |