equal
deleted
inserted
replaced
119 PDF_VIEWER="$ISABELLE_OPEN" |
119 PDF_VIEWER="$ISABELLE_OPEN" |
120 DVI_VIEWER="$ISABELLE_OPEN" |
120 DVI_VIEWER="$ISABELLE_OPEN" |
121 |
121 |
122 |
122 |
123 ### |
123 ### |
124 ### Rendering information |
124 ### Symbol rendering and abbreviations |
125 ### |
125 ### |
126 |
126 |
127 ISABELLE_SYMBOLS="$ISABELLE_HOME/etc/symbols:$ISABELLE_HOME_USER/etc/symbols" |
127 ISABELLE_SYMBOLS="$ISABELLE_HOME/etc/symbols:$ISABELLE_HOME_USER/etc/symbols" |
|
128 ISABELLE_ABBREVS="$ISABELLE_HOME/etc/abbrevs:$ISABELLE_HOME_USER/etc/abbrevs" |
128 |
129 |
129 |
130 |
130 ### |
131 ### |
131 ### Misc old-style settings |
132 ### Misc old-style settings |
132 ### |
133 ### |