[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
bug#45272: [PATCH v3] gnu: gnome-builder: Disable jedi plugin.
From: |
Leo Prikler |
Subject: |
bug#45272: [PATCH v3] gnu: gnome-builder: Disable jedi plugin. |
Date: |
Sat, 19 Dec 2020 12:50:01 +0100 |
As pointed out in #45272, it is broken.
* gnu/packages/gnome.scm (gnome-builder)[#:configure-flags] Add
-Dplugin_jedi=false.
---
gnu/packages/gnome.scm | 3 +++
1 file changed, 3 insertions(+)
diff --git a/gnu/packages/gnome.scm b/gnu/packages/gnome.scm
index 5a166d1b86..f90c0b92a6 100644
--- a/gnu/packages/gnome.scm
+++ b/gnu/packages/gnome.scm
@@ -11876,6 +11876,9 @@ libraries. Applications do not need to be
recompiled--or even restarted.")
"-Dplugin_clang=false"
"-Dplugin_flatpak=false"
"-Dplugin_glade=false"
+ ;; XXX: This one has been shown not to work in
+ ;; <https://issues.guix.gnu.org/45272>
+ "-Dplugin_jedi=false"
;; ... except this one.
"-Dplugin_update_manager=false")
#:phases
--
2.29.2