Re: make info fails without preceding make doc

2021-09-22 Thread Jean Abou Samra
Le 22/09/2021 à 14:02, David Kastrup a écrit : Federico Bruni writes: Il giorno mar 21 set 2021 alle 22:48:04 +0200, David Kastrup ha scritto: "make doc-clean" appears to work better. I find it somewhat surprising that it should not have been implied by "make clean". IIRC it's implied by m

Re: make info fails without preceding make doc

2021-09-22 Thread David Kastrup
Federico Bruni writes: > Il giorno mar 21 set 2021 alle 22:48:04 +0200, David Kastrup > ha scritto: >> "make doc-clean" appears to work better. I find it somewhat >> surprising >> that it should not have been implied by "make clean". > > IIRC it's implied by make distclean At any rate, the Mak

Re: make info fails without preceding make doc

2021-09-22 Thread David Kastrup
Federico Bruni writes: > Il giorno mar 21 set 2021 alle 22:48:04 +0200, David Kastrup > ha scritto: >> "make doc-clean" appears to work better. I find it somewhat >> surprising >> that it should not have been implied by "make clean". > > IIRC it's implied by make distclean Well, but distclean

Re: make info fails without preceding make doc

2021-09-22 Thread Federico Bruni
Il giorno mar 21 set 2021 alle 22:48:04 +0200, David Kastrup ha scritto: "make doc-clean" appears to work better. I find it somewhat surprising that it should not have been implied by "make clean". IIRC it's implied by make distclean ___ bug-li