Tool name: How to avoid duplication of server name?

This issue originates from a discussion on Discord

• A new tool already contains its server's name. eg- github_create_pull_request
• User registers the mcp server in mcpjungle
• Now this tool is registered as github__github_create_pull_request
• The tool name now contains unnecessary duplication of github. Degrades user experience.

Feedback from the user:

"hm if it's using the names as uid then my only suggestion would be to compare all tools at startup/server reg and if none have identical names then skip the prefixes entirely, otherwise warn regarding identicals and add all prefixes. Or even better allow users to define custom tool names and map them to the tools registered with mcp jungle, so only checking uniqueness at the definition point.

I only bring it up because my frontend also suffixes the tool names with the mcp server, so by the time my model is calling the tools they are appX__appX_tool_name_here_mcp_mcpjungle :D"