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

[Leo Prikler]

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