1 files changed, 1 insertions, 0 deletions

diff --git a/_tags b/_tags
index 6c69011b82..6ffe3a8374 100644
--- a/_tags
+++ b/_tags
@@ -79,5 +79,6 @@
 "tools": include
 "tools/coqdoc": include
 "toplevel": include
+"toplevel/utils": include
 
 <plugins/**>: include
\ No newline at end of file