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

Get rid of __GAPINTERNAL_LOADED_FROM_GAP #368

Merged

Conversation

fingolfin
Copy link
Member

No description provided.

@codecov
Copy link

codecov bot commented Mar 11, 2020

Codecov Report

Merging #368 into master will not change coverage by %.
The diff coverage is 100.00%.

@@           Coverage Diff           @@
##           master     #368   +/-   ##
=======================================
  Coverage   77.77%   77.77%           
=======================================
  Files          59       59           
  Lines        4441     4441           
=======================================
  Hits         3454     3454           
  Misses        987      987           
Impacted Files Coverage Δ
pkg/GAPJulia/JuliaInterface/read.g 100.00% <ø> (ø)
src/GAP.jl 88.33% <100.00%> (+0.19%) ⬆️

@fingolfin fingolfin merged commit dcbcba7 into oscar-system:master Mar 11, 2020
@fingolfin fingolfin deleted the mh/__GAPINTERNAL_LOADED_FROM_GAP branch March 11, 2020 23:54
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.

1 participant