Zulip Chat Archive

Stream: general

Topic: Author on normal.lean?


Thomas Browning (Mar 18 2021 at 17:52):

The recent discussions on authors got me thinking. The last 75% of normal.lean was originally contributed by Patrick Lutz and I as part of the abel-ruffini project. Should I add our names to the authors list so that it's clear who to contact about that stuff?

Johan Commelin (Mar 18 2021 at 18:03):

I certainly think that the two of you deserve to be on that list (-;

Scott Morrison (Mar 18 2021 at 21:52):

Maybe we should be thinking of the Authors: list more as "these are the people on the hook when problems come up". So "deserve" is a loaded term. :-)

Mario Carneiro (Mar 19 2021 at 21:03):

I think the people on the hook when problems come up are the maintainers. Stuff that will cause problems for the maintainers are supposed to be caught during review


Last updated: Dec 20 2023 at 11:08 UTC