#1397: Use tini as entrypoint in our Docker image

Closes #1397 (closed)

@mcastril I had said before that Docker was able to magically use tini, and it's indeed true, with docker --init. But on this MR we force that even if the user does not use --tini. We install tini with apt-get (Docker has tini outside of the image), and then run tini -- $old-entry-point. That's all it takes to have tini as root PID, reaping for zombies (it's limited if compared to systemd, but it does reap).

Whoever reviews this, here's how I tested it locally:

$ cd docker
$ docker build -t kinow/autosubmit-4.1.11-dev .
$ docker run --rm -ti kinow/autosubmit-4.1.11-dev /bin/bash
$ autosubmit> # try some commands if you'd like
$ docker run --rm -ti kinow/autosubmit-4.1.11-dev
$ docker run --rm -ti kinow/autosubmit-4.1.11-dev autosubmit -v
# warnings... that we will fix later, ignore
4.1.10

Cheers