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

bib: add a bunch of DOIs, minor corrections #4317

Merged
merged 1 commit into from
Nov 15, 2024
Merged

bib: add a bunch of DOIs, minor corrections #4317

merged 1 commit into from
Nov 15, 2024

Conversation

fingolfin
Copy link
Member

@fingolfin fingolfin commented Nov 15, 2024

DOIs added via script from https://tex.stackexchange.com/a/300474. The DOIs were then checked with https://www.doi2bib.org and in a few cases further adjustments were made to the bib data.

Some progress towards #4214.

DOIs added via script from <https://tex.stackexchange.com/a/300474>.
The DOIs were then checked with <https://www.doi2bib.org> and in a
few cases further adjustments were made to the bib data.
Copy link
Member

@lgoettgens lgoettgens left a comment

Choose a reason for hiding this comment

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

Thanks! Two minor comments

number = {11},
pages = {4491--4535},
year = {2023},
month = jun,
Copy link
Member

Choose a reason for hiding this comment

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

Suggested change
month = jun,

we usually don't keep track of months, and here it is formatted differently as all other fields

Copy link
Member

Choose a reason for hiding this comment

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

If we usually don't keep track of months, shouldn't bibtool be configured to delete the fields?

Copy link
Member

Choose a reason for hiding this comment

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

There are months in the bibliography, but there is a wild mix of formatting already in there:

  month         = {Mar},
  month         = {1},
  month         = jun,
  month         = {mar},

Thus I would keep this PR as is and instead convert this to a new issue that deals with unifying the month fields or deciding to delete them (both using appropriate bibtool settings).

volume = {409},
pages = {108646},
year = {2022},
month = nov,
Copy link
Member

Choose a reason for hiding this comment

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

Suggested change
month = nov,

Copy link

codecov bot commented Nov 15, 2024

Codecov Report

All modified and coverable lines are covered by tests ✅

Project coverage is 84.49%. Comparing base (499f7ce) to head (d38be0d).
Report is 1 commits behind head on master.

Additional details and impacted files
@@            Coverage Diff             @@
##           master    #4317      +/-   ##
==========================================
- Coverage   84.49%   84.49%   -0.01%     
==========================================
  Files         645      645              
  Lines       85589    85589              
==========================================
- Hits        72321    72319       -2     
- Misses      13268    13270       +2     
Files with missing lines Coverage Δ
src/Combinatorics/Matroids/ChowRings.jl 99.20% <ø> (ø)

... and 1 file with indirect coverage changes

@lgoettgens lgoettgens added the documentation Improvements or additions to documentation label Nov 15, 2024
@lgoettgens lgoettgens merged commit fb767f2 into master Nov 15, 2024
30 checks passed
@lgoettgens lgoettgens deleted the mh/doi branch November 15, 2024 13:07
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
documentation Improvements or additions to documentation
Projects
None yet
Development

Successfully merging this pull request may close these issues.

3 participants