diff options
| author | Alec Theriault <alec.theriault@gmail.com> | 2018-11-10 16:02:13 -0800 |
|---|---|---|
| committer | Alec Theriault <alec.theriault@gmail.com> | 2018-11-10 16:02:13 -0800 |
| commit | 959033d592b41235896402a64703650df77c34bd (patch) | |
| tree | 352d1c64c354017adc5b7c3c6aa7aa7fd95e1bf6 /doc | |
| parent | b62c9542480d629bb482f5394dec2fdd5a48af24 (diff) | |
| parent | f4d53a159642aa9182241259709659e7074425d5 (diff) | |
Merge branch 'ghc-8.6' into ghc-head
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 e6612000..c6296089 100644 --- a/doc/invoking.rst +++ b/doc/invoking.rst @@ -330,7 +330,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: @@ -342,11 +342,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. |