|
From: | Ludovic Courtès |
Subject: | bug#45272: [PATCH] gnu: gnome-builder: Disable jedi plugin. |
Date: | Fri, 18 Dec 2020 17:49:51 +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. 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’.
[Prev in Thread] | Current Thread | [Next in Thread] |