diff options
author | Pierre Sassoulas <pierre.sassoulas@gmail.com> | 2022-05-15 23:30:26 +0200 |
---|---|---|
committer | Pierre Sassoulas <pierre.sassoulas@gmail.com> | 2022-05-16 16:57:17 +0200 |
commit | 20d88d7304075f7e1e1317d841b4ce1a1e1ede64 (patch) | |
tree | e941ca9c2cc732de360efcd112c29c6f1916f083 /doc/conf.py | |
parent | 68ae491ad34c235d0d6b9055c943c98c26e11718 (diff) | |
download | pylint-git-20d88d7304075f7e1e1317d841b4ce1a1e1ede64.tar.gz |
[doc] Better more useful links for ide integration
Co-authored-by: Daniƫl van Noord <13665637+DanielNoord@users.noreply.github.com>
Diffstat (limited to 'doc/conf.py')
-rw-r--r-- | doc/conf.py | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/doc/conf.py b/doc/conf.py index fbd73c664..8561cc3bf 100644 --- a/doc/conf.py +++ b/doc/conf.py @@ -54,6 +54,7 @@ redirects: dict[str, str] = { # "<source>": "<target>" "intro": "index.html", "support": "contact.html", + "user_guide/ide-integration": "installation.html", } # Add any paths that contain templates here, relative to this directory. |