# HG changeset patch # User wenzelm # Date 1477397203 -7200 # Node ID 6e9c22c494c59956cfd8968a9e52886b8f8d9fdc # Parent 17a7543fadada3f65bd15f245a0bc0dd81ea4a7c more informative error (stderr); diff -r 17a7543fadad -r 6e9c22c494c5 src/Pure/Admin/isabelle_cronjob.scala --- a/src/Pure/Admin/isabelle_cronjob.scala Tue Oct 25 12:36:09 2016 +0200 +++ b/src/Pure/Admin/isabelle_cronjob.scala Tue Oct 25 14:06:43 2016 +0200 @@ -183,6 +183,7 @@ res match { case Exn.Res(_) => None case Exn.Exn(exn) => + exn.printStackTrace() val first_line = Library.split_lines(Exn.message(exn)).headOption getOrElse "exception" Some(first_line) }