changeset 76580 | 699d9a219e45 |
parent 76578 | 06b001094ddb |
child 76602 | b5dfe1551637 |
--- a/src/Tools/jEdit/src/document_dockable.scala Tue Dec 06 16:26:59 2022 +0100 +++ b/src/Tools/jEdit/src/document_dockable.scala Tue Dec 06 16:38:50 2022 +0100 @@ -192,7 +192,7 @@ /* controls */ private val document_session = - JEdit_Sessions.document_selector(PIDE.options, autosave = true) + JEdit_Sessions.document_selector(PIDE.options, standalone = true) private val build_button = new GUI.Button("<html><b>Build</b></html>") {