# HG changeset patch # User paulson # Date 1456419214 0 # Node ID 994b8bab5a99dcba2722c3ceff6147dd5485e6cf # Parent 2fc7a8d9c529ca05e7513383eab42424822521f1# Parent e391528eff3bf7ff9af6b78a7a838bf0402b09d8 Merge diff -r 2fc7a8d9c529 -r 994b8bab5a99 etc/options --- a/etc/options Thu Feb 25 16:49:00 2016 +0000 +++ b/etc/options Thu Feb 25 16:53:34 2016 +0000 @@ -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 2fc7a8d9c529 -r 994b8bab5a99 src/Pure/Tools/build.scala --- a/src/Pure/Tools/build.scala Thu Feb 25 16:49:00 2016 +0000 +++ b/src/Pure/Tools/build.scala Thu Feb 25 16:53:34 2016 +0000 @@ -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 =