GNU bug report logs - #45272
GNOME Builder: Global search, autocompletion, documentation don't work

Previous Next

Full log

View this message in rfc822 format

From: Leo Prikler <leo.prikler <at> student.tugraz.at>
To: Ludovic Courtès <ludo <at> gnu.org>
Cc: 45272 <at> debbugs.gnu.org, luis.felipe.la <at> protonmail.com
Subject: bug#45272: [PATCH] gnu: gnome-builder: Disable jedi plugin.
Date: Fri, 18 Dec 2020 18:10:02 +0100

Am Freitag, den 18.12.2020, 17:49 +0100 schrieb Ludovic Courtès:
> Hi!
> 
> Leo Prikler <leo.prikler <at> 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

Previous Next

GNU bug tracking system
Copyright (C) 1999 Darren O. Benham, 1997,2003 nCipher Corporation Ltd, 1994-97 Ian Jackson.