From 30076f81448721c49b86846de638cbc936c085fb Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Tue, 17 Feb 2015 21:38:13 +0100
Subject: Separate index for vernacular options.
---
doc/refman/menu.html | 5 ++++-
1 file changed, 4 insertions(+), 1 deletion(-)
(limited to 'doc/refman/menu.html')
diff --git a/doc/refman/menu.html b/doc/refman/menu.html
index db19678f3c..7312ad344c 100644
--- a/doc/refman/menu.html
+++ b/doc/refman/menu.html
@@ -19,6 +19,9 @@ Tactics Index
|
Vernacular Commands Index
|
+
+Vernacular Options Index
+ |
Index of Error Messages
|
@@ -26,4 +29,4 @@ Index of Error Messages
-