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 ### Symbol rendering and abbreviations |
124 ### Symbol rendering |
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" |
|
129 |
128 |
130 |
129 |
131 ### |
130 ### |
132 ### Misc settings |
131 ### Misc settings |
133 ### |
132 ### |