bug#45272: [PATCH] gnu: gnome-builder: Disable jedi plugin.

[Ludovic Courtès]

Hi!

Leo Prikler <leo.prik...@student.tugraz.at> skribis:

> As pointed out in #45272, it is broken.

Please add this as a comment above “-Dplugin_jedi=false” (refer to the
bug by URL so there’s no ambiguity).

> * gnu/packages/gnome.scm (gnome-builder)[#:configure-flags] Add
> -Dplugin_jedi=false.

Otherwise LGTM, thanks!

Ludo’.