src/Tools/jEdit/src/jedit_editor.scala
changeset 56457 eea4bbe15745
parent 56413 2d4d9a5f68ff
child 56458 a8d960baa5c2
     1.1 --- a/src/Tools/jEdit/src/jedit_editor.scala	Mon Apr 07 16:37:57 2014 +0200
     1.2 +++ b/src/Tools/jEdit/src/jedit_editor.scala	Mon Apr 07 21:23:02 2014 +0200
     1.3 @@ -52,7 +52,7 @@
     1.4    {
     1.5      Swing_Thread.require()
     1.6  
     1.7 -    JEdit_Lib.jedit_buffer(name.node) match {
     1.8 +    JEdit_Lib.jedit_buffer(name) match {
     1.9        case Some(buffer) =>
    1.10          PIDE.document_model(buffer) match {
    1.11            case Some(model) => model.snapshot