equal
deleted
inserted
replaced
50 var _return_code: Option[Int] = None |
50 var _return_code: Option[Int] = None |
51 def maybe_exit() |
51 def maybe_exit() |
52 { |
52 { |
53 _return_code match { |
53 _return_code match { |
54 case None => |
54 case None => |
55 case Some(0) => start |
55 case Some(0) => |
56 case Some(rc) => sys.exit(rc) |
56 visible = false |
|
57 default_thread_pool.submit(() => start) |
|
58 case Some(rc) => |
|
59 sys.exit(rc) |
57 } |
60 } |
58 } |
61 } |
59 |
62 |
60 def return_code(rc: Int): Unit = |
63 def return_code(rc: Int): Unit = |
61 Swing_Thread.later { |
64 Swing_Thread.later { |