From 20dd2183d28f20abcee8862fba0ab6a68e153433 Mon Sep 17 00:00:00 2001 From: Steve McIntyre Date: Sun, 26 Mar 2023 23:10:17 +0100 Subject: [PATCH] Remove long-dead docs reference to need-complete-mirror --- docs/makefile.html | 4 ---- 1 file changed, 4 deletions(-) diff --git a/docs/makefile.html b/docs/makefile.html index b35e5e9d..fc7a5e5c 100644 --- a/docs/makefile.html +++ b/docs/makefile.html @@ -38,10 +38,6 @@ all), so simply print a message and return.

ok:

Simple sanity checking.

-

$(MIRROR)/doc:, $(MIRROR)/tools: and -need-complete-mirror

-

Ensure that we have all the needed pieces of the archive.

-

General initialisation and cleanup

init: