zepinto
|
f117dcbe5f
|
Docker Makefile: added DNS option.
# Conflicts:
# docker/Makefile
|
2019-02-11 20:00:17 +00:00 |
|
Pedro Gonçalves
|
f1185813ca
|
docker: fix option to delete docker img.
|
2018-12-12 14:37:05 +00:00 |
|
Pedro Gonçalves
|
2b96c6f84a
|
docker: add option to delete docker system img.
|
2018-12-12 14:27:26 +00:00 |
|
Pedro Gonçalves
|
ed1e4c0240
|
docker/Makefile: add option to clean folder temp/image of docker.
|
2017-06-28 13:37:15 +01:00 |
|
Pedro Gonçalves
|
e0a8b77db3
|
docker: update file to use gcc 5.4.
|
2017-06-28 13:25:37 +01:00 |
|
Tiago Marques
|
4161caff37
|
Dockerfile: Bumped Debian version to 9.
|
2017-05-16 17:38:48 +01:00 |
|
Ricardo Martins
|
62730377b2
|
docker: install file package.
|
2016-06-14 18:54:37 +01:00 |
|
Ricardo Martins
|
4ff07d69e0
|
docker: added script to create docker container suitable to build GLUED.
|
2016-06-03 14:23:22 +01:00 |
|