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