aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--doc/ProofGeneral.texi1
1 files changed, 0 insertions, 1 deletions
diff --git a/doc/ProofGeneral.texi b/doc/ProofGeneral.texi
index 8919f152..304b1dce 100644
--- a/doc/ProofGeneral.texi
+++ b/doc/ProofGeneral.texi
@@ -1848,7 +1848,6 @@ mechanisms if you want to do this.
* Automatic multiple file handling::
* Escaping script management::
* Editing features::
-* Experimental features::
@end menu
@node Document centric working