summaryrefslogtreecommitdiff
path: root/doc/conf.py
diff options
context:
space:
mode:
authorPierre Sassoulas <pierre.sassoulas@gmail.com>2022-05-15 23:30:26 +0200
committerPierre Sassoulas <pierre.sassoulas@gmail.com>2022-05-16 16:57:17 +0200
commit20d88d7304075f7e1e1317d841b4ce1a1e1ede64 (patch)
treee941ca9c2cc732de360efcd112c29c6f1916f083 /doc/conf.py
parent68ae491ad34c235d0d6b9055c943c98c26e11718 (diff)
downloadpylint-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.py1
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.