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

Update Hecke banner #1675

Merged
merged 2 commits into from
Nov 7, 2024
Merged

Update Hecke banner #1675

merged 2 commits into from
Nov 7, 2024

Conversation

paemurru
Copy link
Contributor

@paemurru paemurru commented Nov 6, 2024

I only recently found out that Hecke has its own manual. I included the manual link in the banner, similarly to the Julia and OSCAR banners.

Copy link

codecov bot commented Nov 6, 2024

Codecov Report

Attention: Patch coverage is 0% with 12 lines in your changes missing coverage. Please review.

Project coverage is 75.97%. Comparing base (8564bb0) to head (6b2f6ee).
Report is 3 commits behind head on master.

Files with missing lines Patch % Lines
src/Hecke.jl 0.00% 12 Missing ⚠️
Additional details and impacted files
@@             Coverage Diff             @@
##           master    #1675       +/-   ##
===========================================
+ Coverage    6.54%   75.97%   +69.42%     
===========================================
  Files         361      361               
  Lines      113587   113876      +289     
===========================================
+ Hits         7438    86515    +79077     
+ Misses     106149    27361    -78788     
Files with missing lines Coverage Δ
src/Hecke.jl 51.11% <0.00%> (+8.72%) ⬆️

... and 320 files with indirect coverage changes

@thofma
Copy link
Owner

thofma commented Nov 6, 2024

I did not count, but does this fit a terminal with 80 characters?

@paemurru
Copy link
Contributor Author

paemurru commented Nov 6, 2024

Yes, it is 73 characters wide

@thofma thofma merged commit 39fc9cb into thofma:master Nov 7, 2024
17 checks passed
@paemurru paemurru deleted the ep/update_banner branch November 7, 2024 21:20
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