proper option process_output_tail, more generous default;
authorwenzelm
Thu Feb 25 16:16:29 2016 +0100 (2016-02-25)
changeset 62409e391528eff3b
parent 62408 86f27b264d3d
child 62411 994b8bab5a99
child 62412 ffdc5cf36dc5
child 62423 2497c966ba2b
proper option process_output_tail, more generous default;
etc/options
src/Pure/Tools/build.scala
     1.1 --- a/etc/options	Thu Feb 25 13:58:48 2016 +0000
     1.2 +++ b/etc/options	Thu Feb 25 16:16:29 2016 +0100
     1.3 @@ -96,7 +96,10 @@
     1.4    -- "scale factor for session timeout"
     1.5  
     1.6  option process_output_limit : int = 100
     1.7 -  -- "build process output limit in million characters (0 = unlimited)"
     1.8 +  -- "build process output limit (in million characters, 0 = unlimited)"
     1.9 +
    1.10 +option process_output_tail : int = 40
    1.11 +  -- "build process output tail shown to user (in lines, 0 = unlimited)"
    1.12  
    1.13  
    1.14  section "ML System"
     2.1 --- a/src/Pure/Tools/build.scala	Thu Feb 25 13:58:48 2016 +0000
     2.2 +++ b/src/Pure/Tools/build.scala	Thu Feb 25 16:16:29 2016 +0100
     2.3 @@ -880,9 +880,10 @@
     2.4              val process_result_tail =
     2.5              {
     2.6                val lines = process_result.out_lines.filterNot(_.startsWith("\f"))
     2.7 -              val tail = lines.drop(lines.length - 20 max 0)
     2.8 +              val tail = job.info.options.int("process_output_tail")
     2.9 +              val lines1 = if (tail == 0) lines else lines.drop(lines.length - tail max 0)
    2.10                process_result.copy(out_lines =
    2.11 -                "(see also " + (output_dir + log(name)).file.toString + ")" :: tail)
    2.12 +                "(see also " + (output_dir + log(name)).file.toString + ")" :: lines1)
    2.13              }
    2.14  
    2.15              val heap =