diff options
| author | Mohammad Akhlaghi <mohammad@akhlaghi.org> | 2020-11-13 19:11:18 +0000 |
|---|---|---|
| committer | Mohammad Akhlaghi <mohammad@akhlaghi.org> | 2020-11-13 19:11:18 +0000 |
| commit | 9cfb8d30a7e0fc92dc60f4dad30efc7231b363dc (patch) | |
| tree | efb81da874ae4fc1e73cec5707a8b9e5cb3dee73 /reproduce/analysis/make/top-prepare.mk | |
| parent | 2b39a67c571d1b6ea2375f65be6bf55831e4eaac (diff) | |
README.md: added commands to delete all Docker images
Until now we had described the basic commands on how to create and use
Docker images, but we hadn't mentioned how you can delete them.
With this commit the commands necessary for deleting Docker images have
also been added at the bottom of the section on Docker.
Diffstat (limited to 'reproduce/analysis/make/top-prepare.mk')
0 files changed, 0 insertions, 0 deletions