etc/options

--- a/etc/options	Sat Nov 07 20:04:09 2015 +0100
+++ b/etc/options	Sun Nov 08 14:41:07 2015 +0100
@@ -92,6 +92,9 @@
 option timeout : real = 0
   -- "timeout for session build job (seconds > 0)"
 
+option timeout_scale : real = 1.0
+  -- "scale factor for session timeout"
+
 option process_output_limit : int = 100
   -- "build process output limit in million characters (0 = unlimited)"