summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorLeo Prikler <leo.prikler@student.tugraz.at>2020-12-19 12:50:01 +0100
committerLudovic Courtès <ludo@gnu.org>2020-12-21 17:47:35 +0100
commitf3e0dc63e18c4f4acce1b1d336d23a90beccb77a (patch)
tree4d7378ce088aec6e93f4cfe2c2e3ece909b607a9
parent527551287011888c2ba13fe92e636300ce625430 (diff)
gnu: gnome-builder: Disable jedi plugin.
As pointed out in #45272, it is broken. * gnu/packages/gnome.scm (gnome-builder)[#:configure-flags] Add -Dplugin_jedi=false. Signed-off-by: Ludovic Courtès <ludo@gnu.org>
-rw-r--r--gnu/packages/gnome.scm3
1 files changed, 3 insertions, 0 deletions
diff --git a/gnu/packages/gnome.scm b/gnu/packages/gnome.scm
index 3d99b49ae2..f7263b5841 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