diff options
| author | Maxime Dénès | 2015-02-17 21:38:13 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2015-02-17 21:38:13 +0100 |
| commit | 30076f81448721c49b86846de638cbc936c085fb (patch) | |
| tree | caf0b8313f44fdadb5ccbd1b058a8d485fa9d9d5 /doc/refman/menu.html | |
| parent | 9d141fe86f68f2de7058d317874edc4c0885ebc6 (diff) | |
Separate index for vernacular options.
Diffstat (limited to 'doc/refman/menu.html')
| -rw-r--r-- | doc/refman/menu.html | 5 |
1 files changed, 4 insertions, 1 deletions
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 <TD><CENTER><A HREF="command-index.html" TARGET="UP"><FONT SIZE=2> Vernacular Commands Index </FONT></A></CENTER></TD> +<TD><CENTER><A HREF="option-index.html" TARGET="UP"><FONT SIZE=2> +Vernacular Options Index +</FONT></A></CENTER></TD> <TD><CENTER><A HREF="error-index.html" TARGET="UP"><FONT SIZE=2> Index of Error Messages </FONT></A></CENTER></TD> @@ -26,4 +29,4 @@ Index of Error Messages </CENTER> -</BODY></HTML>
\ No newline at end of file +</BODY></HTML> |