# HG changeset patch
# User wenzelm
# Date 1476778282 -7200
# Node ID 6aefa7e66888286d05ecd3b2f13f99d146c718da
# Parent  303976a45afea9bd196e8adeaf59e136752ed310
avoid spamming log file;

diff -r 303976a45afe -r 6aefa7e66888 src/Pure/Admin/isabelle_cronjob.scala
--- a/src/Pure/Admin/isabelle_cronjob.scala	Tue Oct 18 10:05:38 2016 +0200
+++ b/src/Pure/Admin/isabelle_cronjob.scala	Tue Oct 18 10:11:22 2016 +0200
@@ -172,7 +172,9 @@
       val err =
         res match {
           case Exn.Res(_) => None
-          case Exn.Exn(exn) => Some(Exn.message(exn))
+          case Exn.Exn(exn) =>
+            val first_line = Library.split_lines(Exn.message(exn)).headOption getOrElse "exception"
+            Some(first_line)
         }
       logger.log_end(end_date, err)
     }