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 /doc | |
| parent | 2e3fcd691a66683ea3d043c7c7bafbf1bcdfecf4 (diff) | |
| parent | 0744762fdd835ff192da72b4fc711ffa403ff8ca (diff) | |
Merge PR #7533: [sphinx] Bump timeout. Closes #7532.
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/tools/coqrst/coqdoc/main.py | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/tools/coqrst/coqdoc/main.py b/doc/tools/coqrst/coqdoc/main.py index a004959eb..cedd60d3b 100644 --- a/doc/tools/coqrst/coqdoc/main.py +++ b/doc/tools/coqrst/coqdoc/main.py @@ -40,7 +40,7 @@ def coqdoc(coq_code, coqdoc_bin=None): os.write(fd, COQDOC_HEADER.encode("utf-8")) os.write(fd, coq_code.encode("utf-8")) os.close(fd) - return check_output([coqdoc_bin] + COQDOC_OPTIONS + [filename], timeout = 2).decode("utf-8") + return check_output([coqdoc_bin] + COQDOC_OPTIONS + [filename], timeout = 10).decode("utf-8") finally: os.remove(filename) |