DEV: make pool terminate on exit

Currently, closing the pool on keyboard interrupt can be very slow for long likelihood evaluation times which can cause problems with checkpointing on some clusters.

added <10 lines Infrastructure labels

added 4 commits

• 7bc0ffbd...23159d45 - 3 commits from branch master
• ffc7b8e2 - DEV: make pool terminate on exit

Compare with previous version

approved this merge request

added 9 commits

• ffc7b8e2...c965f842 - 8 commits from branch master
• 5c928095 - DEV: make pool terminate on exit

Compare with previous version

changed milestone to %2.2.1

requested review from @michael.williams

approved this merge request

added 6 commits

• 5c928095...6c6201d7 - 5 commits from branch master
• 2f53006d - DEV: make pool terminate on exit

Compare with previous version

enabled an automatic merge when the pipeline for 2f53006d succeeds

merged

mentioned in merge request !1305 (merged)

mentioned in merge request !1306 (merged)