tree 16c9b228f59bc6d2f4d1d56277c9a3fc587c4820
parent 71d06faabffa63fca4d2adc493a64eab5bb47986
author Davide Pesavento <davidepesa@gmail.com> 1694914236 -0400
committer Davide Pesavento <davidepesa@gmail.com> 1694914236 -0400

build: add `--without-tools` configure option

Change-Id: Idc10aea140c8863a23dccbb38be1b936d5d0302b