Re: [PATCH 4/4] doc lint: make "lint-docs" non-.PHONY

From: Ævar Arnfjörð Bjarmason <avarab@gmail.com>
Date: Oct 16, 2021, 05:13 UTC
Message-ID: <878ryteekt.fsf@evledraar.gmail.com>
In-Reply-To: <438804d8-eedc-cca5-acbd-5534df601b24@gmail.com>

On Sat, Oct 16 2021, Bagas Sanjaya wrote:

Show 10 quoted lines

> On 15/10/21 19.39, Ævar Arnfjörð Bjarmason wrote:
>> @@ -343,6 +348,7 @@ GIT-ASCIIDOCFLAGS: FORCE
>>               fi
>>     clean:
>> +	$(RM) -rf .build/
>>   	$(RM) *.xml *.xml+ *.html *.html+ *.1 *.5 *.7
>>   	$(RM) *.texi *.texi+ *.texi++ git.info gitman.info
>>   	$(RM) *.pdf
>
> Why did you clean the build directory?

The Documentation/.build directory is added by this patch, for the lint scratch files, but the structure is such that it can be used by other things in the future.