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 |
|
Ricardo Martins
|
4ff07d69e0
|
docker: added script to create docker container suitable to build GLUED.
|
2016-06-03 14:23:22 +01:00 |
|