aboutsummaryrefslogtreecommitdiff
path: root/stm/asyncTaskQueue.ml
diff options
context:
space:
mode:
authorcoqbot-app[bot]2021-02-25 09:59:45 +0000
committerGitHub2021-02-25 09:59:45 +0000
commit26439e3eebc3d0b76d8cf89a71cfd0de07731c26 (patch)
treef50a123e93e990724f9c756b90d0a4660a23e433 /stm/asyncTaskQueue.ml
parent1c80a79ae2824027edeea2439bf7e53298724be8 (diff)
parent94d44211fa918a75482d97cc9498811fcbcda0b2 (diff)
Merge PR #13738: Make sure Ltac2 get cleaned too.
Reviewed-by: gares
Diffstat (limited to 'stm/asyncTaskQueue.ml')
0 files changed, 0 insertions, 0 deletions