diff options
| author | Pierre-Marie Pédrot | 2021-03-06 17:42:15 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2021-03-06 17:42:15 +0100 |
| commit | 0d20fdbd82da5c4008a2d49bbf7aad92ada25227 (patch) | |
| tree | 61cb22cedc163392c294b05352cc4fb972c10525 /doc | |
| parent | 9061480b2071d1ab0ccdd7fefeecf932345634dd (diff) | |
| parent | 2da1eef317464036e3a122368508a5f3e4d21f6d (diff) | |
Merge PR #13586: Support nested timeouts
Reviewed-by: ppedrot
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/changelog/12-misc/13586-nested-timeout.rst | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/doc/changelog/12-misc/13586-nested-timeout.rst b/doc/changelog/12-misc/13586-nested-timeout.rst new file mode 100644 index 0000000000..2c31dc210a --- /dev/null +++ b/doc/changelog/12-misc/13586-nested-timeout.rst @@ -0,0 +1,7 @@ +- **Fixed:** + Fix the timeout facility on Unix to allow for nested timeouts. + Previous behavior on nested timeouts was that an "inner" timeout would replace an "outer" + timeout, so that the outer timeout would no longer fire. With the new behavior, Unix and Windows + implementations should be (approximately) equivalent. + (`#13586 <https://github.com/coq/coq/pull/13586>`_, + by Lasse Blaauwbroek). |