clarify that what miri does not not a reasonable choice for language semantics

[web.git] / ralf / _includes / menu-level.html

diff --git a/ralf/_includes/menu-level.html b/ralf/_includes/menu-level.html
index 28b45c79b2eb5233540d20e4e194eb1bef175129..7e4e5ef38da33c662ca6893bf5de87a4b26c1e83 100644 (file)
--- a/ralf/_includes/menu-level.html
+++ b/ralf/_includes/menu-level.html
@@ -1,5 +1,5 @@
 <ul><!--{% for item in include.menu %}
 <ul><!--{% for item in include.menu %}

-    --><li class="{{ item.class }}"><a class="{{ item.class }}" href="{{ site.baseurl }}{{ item.url | replace: '/index.html','/' }}">{{ item.title }}</a></li><!--
+    --><li class="{{ item.class }}"><a class="{{ item.class }}" href="{{ site.baseurl }}{{ item.url }}">{{ item.title }}</a></li><!--

     {% if item.sub %}
         --><li class="sub">{% include menu-level.html menu=item.sub %}</li><!--
     {% endif %}
     {% if item.sub %}
         --><li class="sub">{% include menu-level.html menu=item.sub %}</li><!--
     {% endif %}