etc/options
changeset 62409 e391528eff3b
parent 62115 57895801cb57
child 62498 5dfcc9697f29
--- 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"