Docker files
These are the Docker files used to create the Docker images published at Docker Hub (and possibly more).
To publish images, use something like:
$ docker push ilegeul/debian:9-gnu-mcu-eclipsecentos
CentOS 64-bits images.
debian
Debian 64-bits images.
debian32
Debian 32-bits images.