changeset 52766 | 36c3c051b355 |
parent 52760 | 8517172b9626 |
child 52800 | 1baa5d19ac44 |
52765:260949bf6529 | 52766:36c3c051b355 |
---|---|
459 |
459 |
460 case Markup.Return_Code(rc) if output.is_exit => |
460 case Markup.Return_Code(rc) if output.is_exit => |
461 if (rc == 0) phase = Session.Inactive |
461 if (rc == 0) phase = Session.Inactive |
462 else phase = Session.Failed |
462 else phase = Session.Failed |
463 |
463 |
464 case _ => bad_output() |
464 case _ => raw_output_messages.event(output) |
465 } |
465 } |
466 } |
466 } |
467 } |
467 } |
468 //}}} |
468 //}}} |
469 |
469 |