On Tue, Dec 8, 2015 at 2:21 AM, Thomas Baruchel <baruc...@gmx.com> wrote: > Thank you to both Mateusz Paprocki and Ondřej Čertík, > > it looks like two of my Pull requests have already been merged after I sent > a message here. > May I assume you (Mateusz Paprocki) have some interest in > identifying/recognizing/detecting > numbers or sequences (which is the purpose of the new sympy.concrete.guess > submodule I want to submit in the remaining pull request)? > May I mention you on Github the next time I want to add something related to > that field (as Ondřej Čertík) explained in his own answer? > > What is the exact string I have to add on Github for mentioning you? Is it > in the body of the message of the pull request that I have to do such a > thing? > > Best regards, and thank you again, tb.
To mention somebody on github, lookup their github username, which is mattpap in Mateusz' case and put @ up front like this: @mattpap. Finally, just put this into any comment or issue or PR description. Ondrej > > -- > You received this message because you are subscribed to the Google Groups > "sympy" group. > To unsubscribe from this group and stop receiving emails from it, send an > email to sympy+unsubscr...@googlegroups.com. > To post to this group, send email to sympy@googlegroups.com. > Visit this group at http://groups.google.com/group/sympy. > To view this discussion on the web visit > https://groups.google.com/d/msgid/sympy/0e906478-5cff-43d8-8bfb-126083236723%40googlegroups.com. > > For more options, visit https://groups.google.com/d/optout. -- You received this message because you are subscribed to the Google Groups "sympy" group. To unsubscribe from this group and stop receiving emails from it, send an email to sympy+unsubscr...@googlegroups.com. To post to this group, send email to sympy@googlegroups.com. Visit this group at http://groups.google.com/group/sympy. To view this discussion on the web visit https://groups.google.com/d/msgid/sympy/CADDwiVBKpGDrDAkRfmc6xesEWPy7S3rikxVwJi3_ReSO8jvGUw%40mail.gmail.com. For more options, visit https://groups.google.com/d/optout.
