Skip to content
Snippets Groups Projects
Commit 6e501784 authored by Allan Blanchard's avatar Allan Blanchard
Browse files

Publications: JS script to close menu on click

parent 7c187841
No related branches found
No related tags found
1 merge request!51Improve (and provide some fixes in) publications and documentation
Pipeline #28582 passed
......@@ -12,7 +12,7 @@ css: publications
<li><a href="#general">Frama-C General</a></li>
{% for category in site.data.publications %}
<li>
<a href="#{{ category.id }}">
<a class="nav-link" href="#{{ category.id }}">
{% if category.short %}
{{ category.short }}
{% else %}
......@@ -22,7 +22,7 @@ css: publications
<ul>
{% for plugin in category.plugins %}
<li>
<a href="#{{ plugin.id }}">
<a class="nav-link" href="#{{ plugin.id }}">
{% if plugin.short %}
{{ plugin.short }}
{% else %}
......@@ -81,4 +81,12 @@ css: publications
</div>
</div>
</div>
</body>
\ No newline at end of file
</body>
<script>
var links = document.getElementsByClassName("nav-link");
var check = document.getElementById("nav-check");
for (let link of links) {
link.addEventListener("click", function() { check.checked = false; });
}
</script>
\ No newline at end of file
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment