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, 25 insertions, 0 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 new file mode 100644 index 000000000000..de8397a57a00 --- /dev/null +++ b/dev-util/gnome-builder/files/3.24.2-jedi-fixes-2.patch @@ -0,0 +1,25 @@ +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 + |