Forget that. That was because I also pushed to a branch. For PRs, we'll have to set up a bot to push to a gitlab branch.
Isuru On Tue, May 21, 2019 at 12:41 AM Isuru Fernando <isu...@gmail.com> wrote: > > Yes, but not by default, one has to setup a bot to do that. Here is how > somebody already did exactly that: > > There's a new feature in gitlab that takes care of this. See > https://docs.gitlab.com/ee/ci/ci_cd_for_external_repos/github_integration.html > > I just created https://gitlab.com/isuruf/sympy/ to mirror my github fork > and created a PR at https://github.com/isuruf/sympy/pull/8. Gitlab CI > status is running there without a bot. > > Isuru > -- 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 https://groups.google.com/group/sympy. To view this discussion on the web visit https://groups.google.com/d/msgid/sympy/CA%2B01voO6YBYqmt9t2JCTR5PGfwh05T%3Dti2bgCyMCNf5c5%2BsBzA%40mail.gmail.com. For more options, visit https://groups.google.com/d/optout.