diff options
| author | Pierre-Marie Pédrot | 2015-02-18 17:27:39 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2015-02-18 17:27:39 +0100 |
| commit | 4bb062f4a66c4ae5a1742e7d99fdc335de0d57a9 (patch) | |
| tree | af8ead1cdc5af3842e683f602177ab4fa2dec9b5 /doc/refman/menu.html | |
| parent | 1be9c4da4d814c29d4ba45b121fda924adc1130e (diff) | |
| parent | 29ba692f0fd25ce87392bbb7494cb62e3b97dc07 (diff) | |
Merge branch 'v8.5'
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> |