Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Make log level default to warn on CLI and Python bindings. #12. #14

Closed
wants to merge 1 commit into from

Conversation

cynthia
Copy link
Contributor

@cynthia cynthia commented Dec 5, 2018

There is a nicer way of doing this, but the expected size of the incision needed for that to happen is probably larger than what can be justified for a minor change like this. For those reasons, patch is done in two places.

There is a nicer way of doing this, but the expected size of the
incision needed for that to happen is probably larger than what
can be justified for a minor change like this.
@krikit
Copy link
Member

krikit commented Dec 5, 2018

Thanks for your job. But as I mentioned here at The last thing, please could you give pull request on develop branch?

@cynthia
Copy link
Contributor Author

cynthia commented Dec 5, 2018

So, one thing I would like to mention here is that if you want pull requests to land on a specific branch you should probably make that the default branch. Otherwise Github will happily default you to master, and you'll get more patches like this.

@krikit
Copy link
Member

krikit commented Dec 5, 2018

As a user, I agree with master as a default branch. But for developers, I think we have to work on develop branch as default. We explained why we think pull request be merged into develop branch here. Please could you give us pull request into develop again, like #15?

If a user meets a sudden change in master branch without release note, it will be inconvenience for him/her.

@cynthia
Copy link
Contributor Author

cynthia commented Dec 5, 2018

This is actually easier to do on your side. It’s a limitation of GH that I can’t edit the PR to land on a different branch, so I suggest you try this:

git checkout develop
git remote add cynthia https://github.com/cynthia/khaiii
git fetch —all
git pull —rebase cynthia warn-default
git push origin develop

This should get what you are asking for - and if GH is smart it should also close this PR.

@krikit
Copy link
Member

krikit commented Dec 6, 2018

Thank you for your effort. I merged what you explained. I had to merge local develop branch into origin develop between your step 4 and 5. At that time, I also added pull request number #14 manually on commit log. But GitHub is not so smart. :( This pull request is not closed automatically. Now I close this issue manually.

Next time you give us a pull request, please set merge branch as develop. Thank you for your effort again.

@krikit krikit closed this Dec 6, 2018
@cynthia
Copy link
Contributor Author

cynthia commented Dec 6, 2018

Thanks! I’ve raised #17 in hope to prevent future incidents like this.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants