diff options
| author | Alec Theriault <alec.theriault@gmail.com> | 2018-10-26 09:02:35 -0700 |
|---|---|---|
| committer | Alec Theriault <alec.theriault@gmail.com> | 2018-10-26 09:02:35 -0700 |
| commit | 223a86e2f7bcf83e0e1e45cea82300a9ed7b9219 (patch) | |
| tree | f51a36d6d8774a85970e50391aa91ff55524cb23 /doc | |
| parent | 88f9060466b7f034d7cf0b60d5380507403def36 (diff) | |
User manual + stuff for building GHC docs
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/invoking.rst | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/doc/invoking.rst b/doc/invoking.rst index acdba9bd..3e6e667a 100644 --- a/doc/invoking.rst +++ b/doc/invoking.rst @@ -295,7 +295,7 @@ The following options are available: reader can switch between themes with browsers that support alternate style sheets, or with the "Style" menu that gets added when the page is loaded. If no themes are specified, then just the - default built-in theme ("Ocean") is used. + default built-in theme ("NewOcean") is used. The path parameter can be one of: @@ -307,11 +307,11 @@ The following options are available: - A *CSS file*: The base name of the file becomes the name of the theme. - - The *name* of a built-in theme ("Ocean" or "Classic"). + - The *name* of a built-in theme ("NewOcean", "Ocean", or "Classic"). .. option:: --built-in-themes - Includes the built-in themes ("Ocean" and "Classic"). Can be + Includes the built-in themes ("NewOcean", "Ocean", and "Classic"). Can be combined with :option:`--theme`. Note that order matters: The first specified theme will be the default. |