Le 20/05/2019 à 15:38, Pavel Sanda a écrit :
On Mon, May 20, 2019 at 12:10:24PM -0000, Guenter Milde wrote:but I wonder: shouldn't we just drop the makefile and stop this very partial distribution that makes no sense?This is my suggestion.I agree, these are primarily dev tools. Pavel
But we do distribute the development/ directory. JMarc
