mirror of
https://github.com/zulip/zulip.git
synced 2025-10-23 04:52:12 +00:00
4a2791e2a3
We need this information in the frontend to:
* Display the 'view in playground' option for locally echoed messages.
* When we add a UI settings for realm admins to configure their
playground choices, we'll need to use these canonicalized aliases
for displaying the option.
Hence, this tweaks the tool which generates pygments_data.json to contain
the data we need.
Bumping major PROVISION_VERSION since folks need to provision in both
directions.
Tests amended.