Help page update.

org.lamport.tla.toolbox.doc/html/model/executing-tlc.html

@@ -239,17 +239,17 @@ then the model will remain <A href="about-models.html#locking">locked</A>.
 
 </p>
 
-<!--
-<h3><A name="auto-lock-time">Maximum tail length of Trace explorer states</A></h3>
+
+<h3><A name="maximum-tail-length">Maximum Tail Length of Trace Explorer States</A></h3>
 <p>
 
 The maximum number of states of a trace that is displayed in the Trace Explorer when
 TLC reports an error.&nbsp; 
 If the trace has more states, only the last ones are shown.&nbsp;
 Double-clicking at the beginning of the trace displays additional states.&nbsp;
-The default value is 1000.&nbsp;
+The default value is 10000.&nbsp;
 
-</p> -->
+</p> 
 <h2><a name="crash">If Something Crashes</a></h2>
 
 <!--