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

Add a bunch of trivial implications #65

Merged
merged 1 commit into from
May 16, 2019

Conversation

fingolfin
Copy link
Member

This makes various "hidden" implications created by DeclareProperty explicit, thus fixing a bunch of warnings that show up if one starts the upcoming GAP 4.11 with the -N command line option, and then loads this package.

For some information on the background of this, see also gap-system/gap#1649 and gap-system/gap#2336

This makes various "hidden" implications created by DeclareProperty
explicit, thus fixing a bunch of warnings that show up if one starts
the upcoming GAP 4.11 with the `-N` command line option, and then
loads this package.

For some information on the background of this, see also
<gap-system/gap#1649> and
<gap-system/gap#2336>
@fingolfin fingolfin requested a review from cdwensley May 16, 2019 12:43
@codecov
Copy link

codecov bot commented May 16, 2019

Codecov Report

Merging #65 into master will increase coverage by 0.01%.
The diff coverage is 100%.

@@            Coverage Diff             @@
##           master      #65      +/-   ##
==========================================
+ Coverage   83.62%   83.63%   +0.01%     
==========================================
  Files          39       39              
  Lines       19447    19460      +13     
==========================================
+ Hits        16262    16275      +13     
  Misses       3185     3185
Impacted Files Coverage Δ
lib/gp2up.gd 100% <100%> (ø) ⬆️
lib/gp2obj.gd 100% <100%> (ø) ⬆️
lib/gp3obj.gd 100% <100%> (ø) ⬆️

Copy link
Collaborator

@cdwensley cdwensley left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Looks fine to me.

@cdwensley cdwensley self-assigned this May 16, 2019
@cdwensley
Copy link
Collaborator

Has there been a change in GitHub?
Why does nothing happen when I click on "Merge pull request"?

@cdwensley
Copy link
Collaborator

GitHub warned me that I was using an old version of Safari - I should have taken notice.
Looks like I can merge in Google Chrome.

@cdwensley cdwensley merged commit 1e8e455 into gap-packages:master May 16, 2019
@fingolfin fingolfin deleted the mh/implications branch July 11, 2019 10:52
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