equal
deleted
inserted
replaced
279 vfs.browser.dock-position=floating |
279 vfs.browser.dock-position=floating |
280 vfs.favorite.0.type=1 |
280 vfs.favorite.0.type=1 |
281 vfs.favorite.0=$ISABELLE_HOME |
281 vfs.favorite.0=$ISABELLE_HOME |
282 vfs.favorite.1.type=1 |
282 vfs.favorite.1.type=1 |
283 vfs.favorite.1=$ISABELLE_HOME_USER |
283 vfs.favorite.1=$ISABELLE_HOME_USER |
|
284 vfs.favorite.2.type=1 |
|
285 vfs.favorite.2=$JEDIT_HOME |
|
286 vfs.favorite.3.type=1 |
|
287 vfs.favorite.3=$JEDIT_SETTINGS |
284 view.antiAlias=standard |
288 view.antiAlias=standard |
285 view.blockCaret=true |
289 view.blockCaret=true |
286 view.caretBlink=false |
290 view.caretBlink=false |
287 view.docking.framework=PIDE |
291 view.docking.framework=PIDE |
288 view.eolMarkers=false |
292 view.eolMarkers=false |