Fix git mixup from ticket #17556

[orlitzky]

In ticket #17556 it looks like we only got the commit from Ralf's fix to the Sage Gymnasium.

I think my branch should still be good, but I can't reopen that ticket.

CC: @rwst @kcrisman @vbraun

Component: symbolics

Branch/Commit: u/mjo/ticket/17731 @ d27f849

Reviewer: Michael Orlitzky

Issue created by migration from https://trac.sagemath.org/ticket/17731

[kcrisman]

comment:1

I'm not sure it works - I can't click on the branch and the mouseover text says "Already merged". Interesting. Volker, any clues here?

[sagetrac-git]

Branch pushed to git repo; I updated commit sha1. New commits:

[sagetrac-git]

Changed commit from 044db1d to d27f849

[orlitzky]

comment:3

I think the branch got deleted after the ticket was closed, but I still have it locally. I just rebased it on develop and pushed it, let's see what happens.

[orlitzky]

Changed branch from u/mjo/ticket/17556 to u/mjo/ticket/17731

[orlitzky]

comment:4

Let's try that again.

[kcrisman]

comment:5

Still shows as merged.

[orlitzky]

comment:6

Sorry Volker, I think this was a false alarm. In ticket #15346 it looked like we were missing a commit from #17556. But really what happened was that one of the develop branch merges deleted lines out from under Ralf, and they wound up being added back rather than getting removed from his branch.

[rwst]

comment:7

I'm pretty sure the problem is confined to #15346, and it's up to me to offer apologies.

[kcrisman]

comment:8

So ... close this?

[kcrisman]

Changed reviewer from Ralf Stephan to Michael Orlitzky

[kcrisman]

Changed author from Michael Orlitzky to none