It's a logical bug that didn't have a doctest; it was found when doing a
computation further down (beyond the use-cases it was tested for). It would
be much easier just to change it for the ticket/issue/PR/etc. It wasn't
long after setting a positive review, but we did find it in the transition
On Thu, 9 Feb 2023, 06:46 'Travis Scrimshaw' via sage-devel, <
sage-devel@googlegroups.com> wrote:
> So we don't have PR for all of the positive reviewed tickets. They are
> just going to be merged? What happens if we found a problem with one of the
> +rev tickets and want to change something?
>
So we don't have PR for all of the positive reviewed tickets. They are just
going to be merged? What happens if we found a problem with one of the +rev
tickets and want to change something?
Best,
Travis
On Thursday, February 9, 2023 at 8:43:28 AM UTC+9 Volker Braun wrote:
> But also: Please d
But also: Please don't merge branches into develop until it is absolutely
necessary for the github transition (issue templates or ci setup)
On Tuesday, February 7, 2023 at 6:23:54 PM UTC+1 Dima Pasechnik wrote:
> We have positively reviewed tickets on trac - do we need to do
> anything, or just
I'll try to get them merged
On Tuesday, February 7, 2023 at 6:23:54 PM UTC+1 Dima Pasechnik wrote:
> We have positively reviewed tickets on trac - do we need to do
> anything, or just wait for the release manager to merge them?
>
> Dima
>
--
You received this message because you are subscribed
