[docgen] Update doc/lean.txt

skip-checks: true
Julian · Jul 23, 2021 · 1c81e34 · 1c81e34
1 parent 00eba9c
commit 1c81e34
Showing 1 changed file with 3 additions and 7 deletions.
diff --git a/doc/lean.txt b/doc/lean.txt
@@ -76,19 +76,15 @@ infoview.enable()                                          *infoview.enable()*
 
 
 
-infoview.make_buffer_focusable()            *infoview.make_buffer_focusable()*
-    Configure the infoview to update when this buffer is active.
-
-
-
 infoview.set_autoopen()                              *infoview.set_autoopen()*
     Set whether a new infoview is automatically opened when entering Lean
     buffers.
 
 
 
-infoview.maybe_autoopen()                          *infoview.maybe_autoopen()*
-    Open an infoview for the current buffer if it isn't already open.
+infoview.set_autoclose()                            *infoview.set_autoclose()*
+    Set whether an infoview is automatically closed when leaving from its last
+    associated Lean file.