I had made a pull request here: https://github.com/sympy/sympy/pull/1709 It was an *EasyToFix* issue; I am just a beginner :)
So, after finally it was good enough to be merged (at least I suppose it was), I get this: *SymPy Bot <https://github.com/sympy/sympy-bot> Summary*: Could not fetch the branch prasoon2211/issue-3428. @prasoon2211 <https://github.com/prasoon2211>: Please make sure that prasoon2211/issue-3428 has been pushed to GitHub and run the sympy-bot tests again. Now, the branch in question has obviously been pushed, since I made the pull request from that branch. Also, on my github profile, I saw 4 similar fetch errors. So, is there something that I should do here? I mean my branch has obviously be pushed. Or is there something wrong with sympy-bot since there were 4 similar errors (that I could see). If it's the latter case, then what about the pull request? Thanks Prasoon Shukla -- You received this message because you are subscribed to the Google Groups "sympy" group. To view this discussion on the web visit https://groups.google.com/d/msg/sympy/-/DLdX2Bg-DysJ. To post to this group, send email to [email protected]. To unsubscribe from this group, send email to [email protected]. For more options, visit this group at http://groups.google.com/group/sympy?hl=en.
