PR #1919: rm docker-clean.sh

hpc · Sep 6, 2024 · f2e5b13 · f2e5b13
1 parent ac2190f
commit f2e5b13
Show file tree

Hide file tree

Showing 4 changed files with 1 addition and 51 deletions.
diff --git a/doc/dev.rst b/doc/dev.rst
@@ -253,12 +253,6 @@ fail or that won’t give you additional information, and not pushing every
 commit (CI tests only the most recent commit in a pushed group). Avoid making
 commits merely to trigger CI.
 
-**Purging Docker cache.** :code:`misc/docker-clean.sh` can be used to purge
-your Docker cache, either by removing all tags or deleting all containers and
-images. The former is generally preferred, as it lets you update only those
-base images that have actually changed (the ones that haven’t will be
-re-tagged).
-
 Issue labeling
 --------------
 

diff --git a/misc/Makefile.am b/misc/Makefile.am
@@ -1 +1 @@
-EXTRA_DIST = docker-clean.sh grep version
+EXTRA_DIST = grep version
diff --git a/misc/docker-clean.sh b/misc/docker-clean.sh
diff --git a/misc/loc b/misc/loc
@@ -283,7 +283,6 @@ find . -type f -a \( \
         -path ./.gitattributes \
      -o -path ./.gitignore \
      -o -path ./VERSION \
-     -o -path ./misc/docker-clean.sh \
      -o -path ./misc/branches-tidy \
      -o -path ./misc/grep \
      -o -path ./misc/loc \) | sort > /tmp/loc.misc
Original file line number	Diff line number	Diff line change
		@@ -1 +1 @@
		EXTRA_DIST = docker-clean.sh grep version
		EXTRA_DIST = grep version