# HG changeset patch
# User wenzelm
# Date 1456413389 -3600
# Node ID e391528eff3bf7ff9af6b78a7a838bf0402b09d8
# Parent  86f27b264d3da58b3bda4aeee579b1e042d3a002
proper option process_output_tail, more generous default;

diff -r 86f27b264d3d -r e391528eff3b etc/options
--- a/etc/options	Thu Feb 25 13:58:48 2016 +0000
+++ b/etc/options	Thu Feb 25 16:16:29 2016 +0100
@@ -96,7 +96,10 @@
   -- "scale factor for session timeout"
 
 option process_output_limit : int = 100
-  -- "build process output limit in million characters (0 = unlimited)"
+  -- "build process output limit (in million characters, 0 = unlimited)"
+
+option process_output_tail : int = 40
+  -- "build process output tail shown to user (in lines, 0 = unlimited)"
 
 
 section "ML System"
diff -r 86f27b264d3d -r e391528eff3b src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Thu Feb 25 13:58:48 2016 +0000
+++ b/src/Pure/Tools/build.scala	Thu Feb 25 16:16:29 2016 +0100
@@ -880,9 +880,10 @@
             val process_result_tail =
             {
               val lines = process_result.out_lines.filterNot(_.startsWith("\f"))
-              val tail = lines.drop(lines.length - 20 max 0)
+              val tail = job.info.options.int("process_output_tail")
+              val lines1 = if (tail == 0) lines else lines.drop(lines.length - tail max 0)
               process_result.copy(out_lines =
-                "(see also " + (output_dir + log(name)).file.toString + ")" :: tail)
+                "(see also " + (output_dir + log(name)).file.toString + ")" :: lines1)
             }
 
             val heap =