diff options
| -rw-r--r-- | debian/patches/0001-Deactivate-sphinx_tabs-extension.patch (renamed from debian/patches/0001-Desactivate-sphinx_tabs-extension.patch) | 2 | ||||
| -rw-r--r-- | debian/patches/series | 2 |
2 files changed, 2 insertions, 2 deletions
diff --git a/debian/patches/0001-Desactivate-sphinx_tabs-extension.patch b/debian/patches/0001-Deactivate-sphinx_tabs-extension.patch index 6c91a23..654a328 100644 --- a/debian/patches/0001-Desactivate-sphinx_tabs-extension.patch +++ b/debian/patches/0001-Deactivate-sphinx_tabs-extension.patch @@ -1,6 +1,6 @@ From: Serge Cohen <serge1cohen@free.fr> Date: Mon, 29 Jan 2018 13:47:14 +0100 -Subject: Desactivate sphinx_tabs extension. +Subject: Deactivate sphinx_tabs extension. --- docs/manual/conf.py | 2 +- diff --git a/debian/patches/series b/debian/patches/series index 4c60f32..5f54e83 100644 --- a/debian/patches/series +++ b/debian/patches/series @@ -1 +1 @@ -0001-Desactivate-sphinx_tabs-extension.patch +0001-Deactivate-sphinx_tabs-extension.patch |