Re: [Maria-developers] Cannot push branch to github

Hi Valentin! I've just replied to your pull request. I can guarantee a time for when it will be reviewed, but it will happen. :) Thanks again for the contribution! Regards, Vicențiu On Fri, 26 May 2017 at 15:54 Valentin Rakush wrote: > Hi Vicențiu, hi Sergei, > > thank you for explanations, ye

Re: [Maria-developers] Cannot push branch to github

Hi Vicențiu, hi Sergei, thank you for explanations, yesterday I have submitted pull request https://github.com/MariaDB/server/pull/398 It does not have assignee or reviewers and I am not sure if somebody will be able to see it. Please have a look. Thank you, Valentin On Thu, May 25, 2017 at 12:

Re: [Maria-developers] Cannot push branch to github

Hi Valentin! The correct way to do a pull request is to create your own fork of the server repository. You don't need any special permissions for that. Afterwards, push your changes to your fork. Finally, click on New pull request button in *your* repository. Select the appropriate branch for the