diff options
| author | Maxime Dénès | 2018-05-02 13:55:01 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2018-05-02 13:55:01 +0200 |
| commit | 0149f2c5930a24ef96861af0d863d7c86341a8db (patch) | |
| tree | a1a93852ebc826828c00f47bac482b9c81ce0bf9 /pretyping/typeclasses_errors.ml | |
| parent | 6062f9f6a3770f967b6d540756063a3992131a6c (diff) | |
Make doc owners also own Makefile.doc
Diffstat (limited to 'pretyping/typeclasses_errors.ml')
0 files changed, 0 insertions, 0 deletions