From 4f8f659157492459289f15a7579671fe84c8b092 Mon Sep 17 00:00:00 2001
From: Basile Desloges <basile.desloges@cea.fr>
Date: Thu, 19 Mar 2020 09:57:03 +0100
Subject: [PATCH] [doc] Add `instantiate/` to the list of ignored folders in
 `doc/`

---
 doc/code/.gitignore | 1 +
 1 file changed, 1 insertion(+)

diff --git a/doc/code/.gitignore b/doc/code/.gitignore
index ef81e4e5daf..05325c534d0 100644
--- a/doc/code/.gitignore
+++ b/doc/code/.gitignore
@@ -11,6 +11,7 @@
 /from/
 /html/
 /impact/
+/instantiate/
 /index.html
 /inout/
 /kernel-doc.ocamldoc
-- 
GitLab