diff options
Diffstat (limited to 'dev-util/gnome-builder/files/3.24.2-jedi-fixes-2.patch')
| -rw-r--r-- | dev-util/gnome-builder/files/3.24.2-jedi-fixes-2.patch | 25 |
1 files changed, 0 insertions, 25 deletions
diff --git a/dev-util/gnome-builder/files/3.24.2-jedi-fixes-2.patch b/dev-util/gnome-builder/files/3.24.2-jedi-fixes-2.patch deleted file mode 100644 index de8397a57a00..000000000000 --- a/dev-util/gnome-builder/files/3.24.2-jedi-fixes-2.patch +++ /dev/null @@ -1,25 +0,0 @@ -From 1d7c6fa60faf9e81f2fa0f93898f8e1cc68da6d4 Mon Sep 17 00:00:00 2001 -From: Christian Hergert <chergert@redhat.com> -Date: Thu, 6 Jul 2017 14:32:52 -0700 -Subject: [PATCH] jedi: ignore non-gir files - -The rnc file is now shipped here, so ignore that when going -through the directory contents. ---- - -diff --git a/plugins/jedi/jedi_plugin.py b/plugins/jedi/jedi_plugin.py -index d257680..25ade14 100644 ---- a/plugins/jedi/jedi_plugin.py -+++ b/plugins/jedi/jedi_plugin.py -@@ -280,6 +280,8 @@ class DocumentationDB(object): - # I would use scandir for better performance, but it requires newer Python - for gir_path in GIR_PATH_LIST: - for gir_file in os.listdir(gir_path): -+ if not gir_file.endswith('.gir'): -+ continue - if gir_file in processed_gir_files: - continue - processed_gir_files[gir_file] = None --- -libgit2 0.26.0 - |