--- a/src/Tools/jEdit/src/plugin.scala Wed Dec 05 11:34:04 2012 +0100
+++ b/src/Tools/jEdit/src/plugin.scala Wed Dec 05 12:22:55 2012 +0100
@@ -95,7 +95,7 @@
model_edits ::: edits
}
}
- PIDE.session.edit(init_edits)
+ PIDE.session.update(init_edits)
}
}