1.1 --- a/etc/settings	Mon Feb 05 14:30:55 2001 +0100
     1.2 +++ b/etc/settings	Mon Feb 05 14:31:49 2001 +0100
     1.3 @@ -42,18 +42,18 @@
     1.4  #ML_OPTIONS="@SMLdebug=/dev/null"
     1.5  #ML_PLATFORM=$(eval $("$ML_HOME/.arch-n-opsys" 2>/dev/null); echo "$HEAP_SUFFIX")
     1.6  
     1.7 +# MLWorks 2.0
     1.8 +#ML_SYSTEM=mlworks
     1.9 +#ML_HOME="$ISABELLE_HOME/../mlworks/bin"
    1.10 +#ML_OPTIONS=""
    1.11 +#ML_PLATFORM=""
    1.12 +
    1.13  # Moscow ML 2.00 or later (experimental!)
    1.14  #ML_SYSTEM=mosml
    1.15  #ML_HOME="$ISABELLE_HOME/../mosml/bin"
    1.16  #ML_PLATFORM=""
    1.17  #ML_OPTIONS=""
    1.18  
    1.19 -# MLWorks 2.0
    1.20 -#ML_SYSTEM=mlworks
    1.21 -#ML_HOME="$ISABELLE_HOME/../mlworks/bin"
    1.22 -#ML_OPTIONS=""
    1.23 -#ML_PLATFORM=""
    1.24 -
    1.25  # Standard ML of New Jersey 0.93
    1.26  #ML_SYSTEM=smlnj-0.93
    1.27  #ML_HOME=/usr/local/ldist/DIR/sml-0.93/src
    1.28 @@ -79,8 +79,11 @@
    1.29  ISABELLE_BIBTEX="bibtex"
    1.30  ISABELLE_DVIPS="dvips -D 600"
    1.31  
    1.32 +# Paranoia setting ...
    1.33 +#unset TEXMF
    1.34 +
    1.35  # The thumbpdf tool is probably not generally available ...
    1.36 -#ISABELLE_THUMBPDF="thumbpdf"
    1.37 +#type -path thumbpdf >/dev/null && ISABELLE_THUMBPDF="thumbpdf"
    1.38  
    1.39  
    1.40  ###
    1.41 @@ -175,7 +178,7 @@
    1.42    "/usr/local/x-symbol" \
    1.43    "/opt/x-symbol" \
    1.44    "")
    1.45 -#required for remote fonts only ...
    1.46 +# Required for remote fonts only ...
    1.47  #XSYMBOL_INSTALLFONTS="xset fp+ tcp/isafonts.informatik.tu-muenchen.de:7200"
    1.48  
    1.49