diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2018-03-18 12:44:03 +0100 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2018-03-20 17:56:30 +0100 |
| commit | 45d8669d4f3cf009ee71c109fafd9d0fc9a9862c (patch) | |
| tree | 4b7b1b1f917eae680c132694660a7ba117c79474 /intf/notation_term.ml | |
| parent | 57877caba02e8e9a950f5302b887970dcb9712a7 (diff) | |
Add CODEOWNERS
See https://help.github.com/articles/about-codeowners/ for
documentation.
Diffstat (limited to 'intf/notation_term.ml')
0 files changed, 0 insertions, 0 deletions