diff options
author | Maxime Dénès <mail@maximedenes.fr> | 2018-05-25 11:01:40 +0200 |
---|---|---|
committer | Maxime Dénès <mail@maximedenes.fr> | 2018-05-25 11:01:40 +0200 |
commit | 8a570b6830d5f42c29c36df13c10a8550120641b (patch) | |
tree | 0d7af2fefc23c08225a4a713e7f4f466bf0ac22a /printing/printer.ml | |
parent | 2e3fcd691a66683ea3d043c7c7bafbf1bcdfecf4 (diff) | |
parent | 0744762fdd835ff192da72b4fc711ffa403ff8ca (diff) |
Merge PR #7533: [sphinx] Bump timeout. Closes #7532.
Diffstat (limited to 'printing/printer.ml')
0 files changed, 0 insertions, 0 deletions