From 5451329b7f82c40bc9beb1afca0cfc37d8598996 Mon Sep 17 00:00:00 2001 From: Jules Aguillon Date: Wed, 27 Nov 2024 17:23:06 +0100 Subject: [PATCH] Update CHANGES --- CHANGES.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/CHANGES.md b/CHANGES.md index 7d061c8985..12dd5eedb3 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -56,7 +56,7 @@ profile. This started with version 0.26.0. - Added back the flag `--disable-outside-detected-project` (#2439, @gpetiot) It was removed in version 0.22. -- Support newer Odoc syntax (#2631, #2632, @Julow) +- Support newer Odoc syntax (#2631, #2632, #2633, @Julow) ### Changed