src/Tools/jEdit/src/jEdit.props
changeset 63751 4fe8cfaeb1fc
parent 63737 fb0ae6b60491
child 63758 a9159d30070f
equal deleted inserted replaced
63750:ebcc70c120a9 63751:4fe8cfaeb1fc
   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