diff options
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). |