[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
bug#45272: [PATCH] gnu: gnome-builder: Disable jedi plugin.
From: |
Leo Prikler |
Subject: |
bug#45272: [PATCH] gnu: gnome-builder: Disable jedi plugin. |
Date: |
Fri, 18 Dec 2020 18:10:02 +0100 |
User-agent: |
Evolution 3.34.2 |
Am Freitag, den 18.12.2020, 17:49 +0100 schrieb Ludovic Courtès:
> 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).
I feel like a side comment as in v2 would be wiser, so as to not
disrupt the sentence started before and to keep the sentiment, that it
should be enabled once someone has figured out, how to do so.
Of course, the side does not offer enough space for the full URL, so
that's bad. Would it suffice to add the URL to the commit message, so
one could `git blame` me?
Regards,
Leo
- bug#45272: GNOME Builder: Global search, autocompletion, documentation don't work, Luis Felipe, 2020/12/16
- bug#45272: GNOME Builder: Global search, autocompletion, documentation don't work, Leo Prikler, 2020/12/18
- bug#45272: [PATCH] gnu: gnome-builder: Disable jedi plugin., Leo Prikler, 2020/12/18
- bug#45272: [PATCH v2] gnu: gnome-builder: Disable jedi plugin., Leo Prikler, 2020/12/18
- bug#45272: [PATCH v3] gnu: gnome-builder: Disable jedi plugin., Leo Prikler, 2020/12/19