{% comment %}Operator extension menu items, already filtered by role on the server (infra.extensions).{% endcomment %} {% for group in ext_nav %}
{% if group.section %}{% endif %} {% for item in group.items %} {{ item.label }} {% endfor %}
{% endfor %}