diff options
Diffstat (limited to '')
| -rw-r--r-- | user/conf.py | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/user/conf.py b/user/conf.py index d22b347..9865a2d 100644 --- a/user/conf.py +++ b/user/conf.py @@ -27,6 +27,7 @@ exclude_patterns = ['config/build.rst', 'installation/prefixes-sandboxing.rst', 'installation/releases.rst', 'installation/developer.rst', + 'installation/kernel.rst', 'tools/build.rst', 'tools/simulation.rst', |