--- 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"
--- 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 =