# 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)
         }