aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar David Aspinall <da@inf.ed.ac.uk>2009-08-07 14:47:19 +0000
committerGravatar David Aspinall <da@inf.ed.ac.uk>2009-08-07 14:47:19 +0000
commit9e51d6adae7df51fec57d3422bfdef991f6fc674 (patch)
treec4d96423ec0815f096dcd2518ee2cbd3acaf853b
parent70770da03bd6c5111279385eaa251867fb60a3e2 (diff)
Remove experimental features node
-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