diff options
| author | Ramiro Morales <ramiro@users.noreply.github.com> | 2018-01-20 14:38:48 -0300 |
|---|---|---|
| committer | Tim Graham <timograham@gmail.com> | 2018-01-20 12:38:48 -0500 |
| commit | 37c17846ad6b02c6dca72e8087a279cca04a0c27 (patch) | |
| tree | 03c6dc058936e14daee338dca6413915dcad8f93 /docs/conf.py | |
| parent | a22ef3bb379a8783d0a2c3d7e1de531dce220a75 (diff) | |
Fixed #28343 -- Add an OS chooser for docs command line examples.
Diffstat (limited to 'docs/conf.py')
| -rw-r--r-- | docs/conf.py | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/docs/conf.py b/docs/conf.py index 639438a3ac..8094cdd2e1 100644 --- a/docs/conf.py +++ b/docs/conf.py @@ -112,7 +112,7 @@ today_fmt = '%B %d, %Y' # List of patterns, relative to source directory, that match files and # directories to ignore when looking for source files. -exclude_patterns = ['_build'] +exclude_patterns = ['_build', '_theme'] # The reST default role (used for this markup: `text`) to use for all documents. # default_role = None |