search

leanprover-community / leanprover-community.github.io

Hosts the website for mathlib and other Lean community infrastructure.
https://leanprover-community.github.io/
MIT License
51 stars 119 forks source link

make sure the example copyright header would pass CI #508

Closed edegeltje closed 1 month ago

edegeltje commented 1 month ago

the linter checking the header matches on Authors: and makes sure the line doesn't end in ., so it would fail on the example. also make the year current, while we're at it.

adomani commented 1 month ago

Maybe you could also mention in the text below that you should use Authors even if there is only one and that there should be no and separating the penultimate and the last author.

edegeltje commented 1 month ago

i took the freedom of suggesting to use commas rather than just discouraging the use of and.

bryangingechen commented 1 month ago

Thank you!