summaryrefslogtreecommitdiff
path: root/.gitignore
diff options
context:
space:
mode:
authorFlorian Angeletti <florian.angeletti@inria.fr>2021-04-07 14:11:43 +0200
committerGitHub <noreply@github.com>2021-04-07 14:11:43 +0200
commit2226776f13761fe670091a1aeb14f5f412a58ca1 (patch)
treee3ef084286052bbce505c5a6e2ab01dda7d3999b /.gitignore
parentd4dd566e3ee5c5fc2ed1b328ccdcf347804cbd66 (diff)
downloadocaml-2226776f13761fe670091a1aeb14f5f412a58ca1.tar.gz
documentation: configuration switch for an odoc documentation mode (#9997)
Diffstat (limited to '.gitignore')
-rw-r--r--.gitignore7
1 files changed, 2 insertions, 5 deletions
diff --git a/.gitignore b/.gitignore
index c2cc6d14be..bfc37866dc 100644
--- a/.gitignore
+++ b/.gitignore
@@ -93,12 +93,9 @@ _build
/manual/src/cmds/warnings-help.etex
/manual/src/warnings-help.etex
-/api_docgen/man
-/api_docgen/html
/api_docgen/build
-/api_docgen/latex
-/api_docgen/texi
-/api_docgen/Compiler_libs.mld
+/api_docgen/odoc/build
+/api_docgen/ocamldoc/build
/ocamldoc/ocamldoc
/ocamldoc/ocamldoc.opt