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 missing citations #41

Merged
merged 6 commits into from
Mar 20, 2024
Merged

Add missing citations #41

merged 6 commits into from
Mar 20, 2024

Conversation

jngrad
Copy link
Contributor

@jngrad jngrad commented Mar 7, 2024

Partial fix for #21

Look for occurrences of REF and substitute with the relevant literature.

@jngrad
Copy link
Contributor Author

jngrad commented Mar 7, 2024

Note to reviewers: this PR incorporates #39, because it contributed a citation that was needed in other places of the text. IIRC merging a PR containing all commits from an older PR should automatically close and mark the older PR as merged. I couldn't push to the older PR due to insufficient rights, and didn't want to create an independent PR that would introduce unnecessary merge conflicts.

@knarrff knarrff merged commit 2805308 into DE-RSE:main Mar 20, 2024
1 check passed
@jngrad jngrad deleted the references branch March 20, 2024 18:36
@jngrad jngrad restored the references branch November 19, 2024 18:16
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.

3 participants