Skip to content

Conversation

mundya
Copy link
Member

@mundya mundya commented Jan 13, 2016

Bug would have meant that removing default entries would not have been attempted if ordered covering failed to produce a table at least as small as the target length.

Bug would have meant that removing default entries would not have been
attempted if ordered covering failed to produce a table at least as
small as the target length.
@mossblaser
Copy link
Member

LGTM!

mossblaser added a commit that referenced this pull request Jan 14, 2016
@mossblaser mossblaser merged commit 169b38c into master Jan 14, 2016
@mossblaser mossblaser deleted the fix-minimisation-bug branch January 14, 2016 08:34
@mundya
Copy link
Member Author

mundya commented Jan 14, 2016

Thanks!

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

Successfully merging this pull request may close these issues.

2 participants