blob: de8397a57a00445e399e12e6ff2298205b9255bc (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
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
|
