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

From: Ævar Arnfjörð Bjarmason <[email-masked]>
Date: Sat, 16 Oct 2021 07:13:28 +0200

On Sat, Oct 16 2021, Bagas Sanjaya wrote:

> 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.