bug-guix
[Top][All Lists]
Advanced
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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

From: Ludovic Courtès
Subject: bug#45272: [PATCH v3] gnu: gnome-builder: Disable jedi plugin.
Date: Mon, 21 Dec 2020 15:30:12 +0100
User-agent: Gnus/5.13 (Gnus v5.13) Emacs/27.1 (gnu/linux) 
Hi,

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

> As pointed out in #45272, it is broken.
>
> * gnu/packages/gnome.scm (gnome-builder)[#:configure-flags] Add
> -Dplugin_jedi=false.

Perfect.  :-)

Applied, thanks!

Ludo’.
reply via email to
[Prev in Thread] Current Thread [Next in Thread]