diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2018-07-16 13:27:08 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2018-07-16 13:27:08 +0200 |
| commit | e27d2fd32e40937e48889772361f1cf53dd9c48e (patch) | |
| tree | 5a5e6aaf009fa5ab5ee1b376ba38dbaa76a2f392 /theories | |
| parent | ad5d90e30d52038c22a5315cbf84aa30aa021875 (diff) | |
| parent | 55f59acbd9cdec6188613edc29e49d5f5a4f6d98 (diff) | |
Merge PR #8023: Introduce a team of code owners for the CI system.
Diffstat (limited to 'theories')
0 files changed, 0 insertions, 0 deletions