Figure out whether we need tini as pid1 in containers

[make-github-pseudonymous-again]

Probably not for MongoDB, probably for web container. See:

• https://stackoverflow.com/questions/56496495/when-not-to-use-docker-run-init
• https://stackoverflow.com/questions/49162358/docker-init-zombies-why-does-it-matter
• What is advantage of Tini? krallin/tini#8 (comment)
• https://stackoverflow.com/questions/34441975/sigterm-does-not-reach-node-script-when-docker-runs-it-with-bin-sh-c/34446294
• https://stackoverflow.com/questions/50356032/whats-the-docker-compose-equivalent-of-docker-run-init
• https://computingpost.medium.com/how-to-use-tini-init-system-in-docker-containers-69283d0099ed

[make-github-pseudonymous-again]

Experiments show that without --init or init: true killing the web service times out. With --init or init: true, the web service is killed immediately. There is no need to use --init or init: true for mongo since it already properly forwards signals.

We could use --init or init: true to take care of potential bugs in mongo, but I have not seen this concern raised anywhere.