aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2018-07-16 13:27:08 +0200
committerGravatar Maxime Dénès <mail@maximedenes.fr>2018-07-16 13:27:08 +0200
commite27d2fd32e40937e48889772361f1cf53dd9c48e (patch)
tree5a5e6aaf009fa5ab5ee1b376ba38dbaa76a2f392 /theories
parentad5d90e30d52038c22a5315cbf84aa30aa021875 (diff)
parent55f59acbd9cdec6188613edc29e49d5f5a4f6d98 (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