diff options
| author | Leo Prikler <leo.prikler@student.tugraz.at> | 2020-12-19 12:50:01 +0100 |
|---|---|---|
| committer | Ludovic Courtès <ludo@gnu.org> | 2020-12-21 17:47:35 +0100 |
| commit | f3e0dc63e18c4f4acce1b1d336d23a90beccb77a (patch) | |
| tree | 4d7378ce088aec6e93f4cfe2c2e3ece909b607a9 | |
| parent | 527551287011888c2ba13fe92e636300ce625430 (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.scm | 3 |
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 |