equal
deleted
inserted
replaced
474 val end_date = Date.now() |
474 val end_date = Date.now() |
475 val err = |
475 val err = |
476 res match { |
476 res match { |
477 case Exn.Res(_) => None |
477 case Exn.Res(_) => None |
478 case Exn.Exn(exn) => |
478 case Exn.Exn(exn) => |
479 Output.writeln("Exception trace for " + quote(task.name) + ":") |
479 Output.writeln("Exception trace for " + quote(task.name) + ":\n" + Exn.trace(exn)) |
480 exn.printStackTrace() |
|
481 val first_line = split_lines(Exn.message(exn)).headOption getOrElse "exception" |
480 val first_line = split_lines(Exn.message(exn)).headOption getOrElse "exception" |
482 Some(first_line) |
481 Some(first_line) |
483 } |
482 } |
484 logger.log_end(end_date, err) |
483 logger.log_end(end_date, err) |
485 } |
484 } |