# HG changeset patch
# User wenzelm
# Date 1677233251 -3600
# Node ID cbd053fff24c0bddd8752e34e6a5901b4d236f10
# Parent  c1c6f895d9ec501dd60ffbec4185a60d6087a5f9
unused (see also 7b318273a4aa and a1fb4d28e609);

diff -r c1c6f895d9ec -r cbd053fff24c etc/options
--- a/etc/options	Wed Feb 22 21:40:32 2023 +0100
+++ b/etc/options	Fri Feb 24 11:07:31 2023 +0100
@@ -132,9 +132,6 @@
 option timeout_build : bool = true
   -- "observe timeout for session build"
 
-option process_output_limit : int = 100
-  -- "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)"