| changeset 55618 | 995162143ef4 |
| parent 54640 | bbd2fa353809 |
| child 55825 | 694833e3e4a0 |
| 55617:2c585bb9560c | 55618:995162143ef4 |
|---|---|
75 react { |
75 react { |
76 case _: Session.Global_Options => |
76 case _: Session.Global_Options => |
77 Swing_Thread.later { handle_resize() } |
77 Swing_Thread.later { handle_resize() } |
78 |
78 |
79 case bad => |
79 case bad => |
80 java.lang.System.err.println("Find_Dockable: ignoring bad message " + bad) |
80 System.err.println("Find_Dockable: ignoring bad message " + bad) |
81 } |
81 } |
82 } |
82 } |
83 } |
83 } |
84 |
84 |
85 override def init() |
85 override def init() |