changeset 53457 | b7c15885fd1e |
parent 53456 | d12be8f62285 |
child 53458 | ddefd18d5ed0 |
53456:d12be8f62285 | 53457:b7c15885fd1e |
---|---|
52 |
52 |
53 _window match { |
53 _window match { |
54 case None => |
54 case None => |
55 case Some(window) => |
55 case Some(window) => |
56 window.visible = false |
56 window.visible = false |
57 window.dispose |
|
57 _window = None |
58 _window = None |
58 } |
59 } |
59 |
60 |
60 try { result.fulfill(_return_code.get) } |
61 try { result.fulfill(_return_code.get) } |
61 catch { case ERROR(_) => } |
62 catch { case ERROR(_) => } |