diff options
| author |  Clément Pit-Claudel <clement.pitclaudel@live.com> | 2018-05-16 17:13:46 +0200 |
|---|---|---|
| committer |  Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr> | 2018-05-16 17:13:46 +0200 |
| commit | 0744762fdd835ff192da72b4fc711ffa403ff8ca (patch) | |
| tree | 52e9fe9d181ed50159e11d3d196971c3da0590e4 /doc/tools | |
| parent | d74d72419f5e9b68fe8ec9e8c046faecacf9f2f4 (diff) | |
[sphinx] Bump timeout. Closes #7532.
Diffstat (limited to 'doc/tools')
| -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) |