aboutsummaryrefslogtreecommitdiff
path: root/tools
diff options
context:
space:
mode:
authorcoqbot-app[bot]2021-04-12 12:34:16 +0000
committerGitHub2021-04-12 12:34:16 +0000
commit271445decd0fc1a37da3009f148f2e68c7168fe1 (patch)
tree631d9976d17d6573b0f348cfd6fdbd83bb779ddb /tools
parent7ce1c4844b077adb25d14cf1bbd2d22548b1e935 (diff)
parent520ac61dfe5a6e865cb7b10f4a822c0d72f3ded9 (diff)
Merge PR #14046: make critical sections safe in the presence of exceptions
Reviewed-by: ejgallego Ack-by: gares Ack-by: SkySkimmer Ack-by: gadmm
Diffstat (limited to 'tools')
0 files changed, 0 insertions, 0 deletions