aboutsummaryrefslogtreecommitdiff
path: root/dev/header.py
AgeCommit message (Collapse)Author
2020-03-18Remove dates in headers.Théo Zimmermann
Cf. discussion at #11559 and decision of Coq Call 2020-02-26.
2019-06-17Update py-style headers to new year.Théo Zimmermann
2018-03-06Standard headers for C and Python.Maxime Dénès