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

From: Ludovic Courtès <[email-masked]>
Date: Fri, 18 Dec 2020 17:49:51 +0100

Hi!

Leo Prikler <[email-masked]> 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’.