Revision 9cfb8d30a7e0fc92dc60f4dad30efc7231b363dc authored by Mohammad Akhlaghi on 13 November 2020, 19:11:18 UTC, committed by Mohammad Akhlaghi on 13 November 2020, 19:11:18 UTC
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.
1 parent 2b39a67
| File | Mode | Size |
|---|---|---|
| reproduce | ||
| tex | ||
| .dir-locals.el | -rw-r--r-- | 1.3 KB |
| .file-metadata | -rw-r--r-- | 9.0 KB |
| .gitignore | -rw-r--r-- | 994 bytes |
| COPYING | -rw-r--r-- | 34.3 KB |
| README-hacking.md | -rw-r--r-- | 90.6 KB |
| README.md | -rw-r--r-- | 18.8 KB |
| paper.tex | -rw-r--r-- | 14.0 KB |
| project | -rwxr-xr-x | 20.1 KB |
Computing file changes ...
