diff -r 4b06a20b13b5 -r 814a1ab42d70 etc/options
--- a/etc/options	Mon Oct 01 19:30:36 2018 +0200
+++ b/etc/options	Tue Oct 02 19:02:47 2018 +0200
@@ -174,7 +174,7 @@
   -- "maximum amount of reparsed text outside perspective"
 
 public option editor_tracing_messages : int = 1000
-  -- "initial number of tracing messages for each command transaction"
+  -- "initial number of tracing messages for each command transaction (0: unbounded)"
 
 public option editor_chart_delay : real = 3.0
   -- "delay for chart repainting"