Hi Marcel, hi Chris,
Am Fr., 5. Apr. 2019 um 08:41 Uhr schrieb Marcel Taeumel < marcel.taeumel@hpi.de>:
The Tools menu is *not* about installing tools but starting them.
Sorry, that was my compromise proposal in the other thread.
Thank you Chris for considering to keep the items around somewhere. But it seems the discussion of where to put them is not over yet.
In the long term, we should find ways to ship such infrastructure in releases without spoiling the (development) trunk.
But if the infrastructure that "spoils" the trunk are development tools, why would you exempt them from the *development* trunk?