ToolDef documentation: rename 'ToolDef tool manual' to 'ToolDef interpreter'
Everytime I visit the ToolDef documentation to look up a builtin tool, I always click on the 'ToolDef tool manual' by mistake. The 'tool manual' is about the ToolDef tooling, the ToolDef interpreter, tough, and not about the built-in tools. Those are described in the language reference manual. I propose:
- Rename the 'ToolDef tool manual' section to 'ToolDef interpreter' section.
Since the ToolDef interpreter is described on a single page that is not very long, it doesn't feel right to call it a 'manual' by itself. And naming it 'ToolDef interpreter' indicates better what information can be found there.