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

Fix ExtendedVectors for trivial vector spaces #2582

Merged
merged 1 commit into from
Jul 2, 2018

Conversation

fingolfin
Copy link
Member

... in case of different method ranking

... in case of different method ranking
@fingolfin fingolfin added kind: bug Issues describing general bugs, and PRs fixing them topic: library labels Jun 27, 2018
@codecov
Copy link

codecov bot commented Jun 27, 2018

Codecov Report

Merging #2582 into master will increase coverage by <.01%.
The diff coverage is 100%.

@@            Coverage Diff             @@
##           master    #2582      +/-   ##
==========================================
+ Coverage    74.6%    74.6%   +<.01%     
==========================================
  Files         481      481              
  Lines      242383   242381       -2     
==========================================
  Hits       180837   180837              
+ Misses      61546    61544       -2
Impacted Files Coverage Δ
lib/vspcrow.gi 78.82% <100%> (+0.2%) ⬆️

@fingolfin fingolfin merged commit b234e0f into gap-system:master Jul 2, 2018
@fingolfin fingolfin deleted the mh/fix-ExtendedVectors branch July 2, 2018 10:03
@fingolfin fingolfin added the release notes: added PRs introducing changes that have since been mentioned in the release notes label Jul 31, 2018
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
kind: bug Issues describing general bugs, and PRs fixing them release notes: added PRs introducing changes that have since been mentioned in the release notes topic: library
Projects
None yet
Development

Successfully merging this pull request may close these issues.

None yet

2 participants