mathlib
ed9ef1b4 - chore(*): normalise copyright headers (#4497)

Commit
5 years ago
chore(*): normalise copyright headers (#4497) This diff makes sure that all files start with a copyright header of the following shape ``` /- Copyright ... ... Apache ... Author... -/ ``` Some files used to have a short description of the contents in the same comment block. Such comments have *not* been turned into module docstrings, but simply moved to a regular comment block below the copyright header. Turning these comments into good module docstrings is an effort that should be undertaken in future PRs.
Author
Parents
Loading