references.bib

Stream: mathlib4

[Christopher Hoskin]

I've opened a PR which adds a new file to mathlib4 (not in mathlib3). I want to add a new reference, but it appears that docs/references.bib is not included in mathlib4 yet.

What should I do with the new reference?

Thanks.

Christopher

[Alex J. Best]

For now doc-gen4 doesn't support references, so I'd say we should do whatever makes it easiest to keep track of new references and port the mathlib 3 ones later. So I vote for make a new stub docs/references.bib for your reference until we finalize how it will work