From fb9200a70a05cbae41af75b60bab7ea2f4ca3fbf Mon Sep 17 00:00:00 2001 From: Paul-Elliot Date: Fri, 13 Dec 2024 16:32:48 +0100 Subject: [PATCH] Doc: add odoc song to index page --- doc/odoc.mld | 2 ++ 1 file changed, 2 insertions(+) diff --git a/doc/odoc.mld b/doc/odoc.mld index 03be72da81..5d4ee6e454 100644 --- a/doc/odoc.mld +++ b/doc/odoc.mld @@ -3,6 +3,8 @@ {0 The [odoc] documentation generator} +{audio:https://choum.net/panglesd/odoc.mp3} + {b For a quick look at the [odoc] syntax, see the {{!cheatsheet}cheatsheet}!} {1:overview What is [odoc]?}