--- a/src/Tools/jEdit/src-base/pide_docking_framework.scala Mon Mar 01 20:12:09 2021 +0100
+++ b/src/Tools/jEdit/src-base/pide_docking_framework.scala Mon Mar 01 22:22:12 2021 +0100
@@ -60,7 +60,7 @@
if (detach_operation.isDefined) {
val detach_item = new JMenuItem("Detach")
detach_item.addActionListener(new ActionListener {
- def actionPerformed(evt: ActionEvent) { detach_operation.get.apply() }
+ def actionPerformed(evt: ActionEvent): Unit = detach_operation.get.apply()
})
menu.add(detach_item)
}