diff options
| author | Théo Zimmermann | 2020-02-18 19:47:40 +0100 |
|---|---|---|
| committer | Théo Zimmermann | 2020-02-18 19:47:40 +0100 |
| commit | f208f65ee8ddb40c9195b5c06475eabffeae0401 (patch) | |
| tree | 3f6e5d9f1c1bffe3e4187131f87d3187a8d9ebe5 /doc/stdlib/dune | |
| parent | af3fd09e2f0cc2eac2bc8802a6818baf0c184563 (diff) | |
| parent | 83052eff43d3eeff96462286b69249ef868bf5f0 (diff) | |
Merge PR #11529: [build] Consolidate stdlib's .v files under a single directory.
Reviewed-by: Zimmi48
Diffstat (limited to 'doc/stdlib/dune')
| -rw-r--r-- | doc/stdlib/dune | 4 |
1 files changed, 1 insertions, 3 deletions
diff --git a/doc/stdlib/dune b/doc/stdlib/dune index 828caecabc..093c7a62b2 100644 --- a/doc/stdlib/dune +++ b/doc/stdlib/dune @@ -5,7 +5,6 @@ (deps make-library-index index-list.html.template hidden-files (source_tree %{project_root}/theories) - (source_tree %{project_root}/plugins) (source_tree %{project_root}/user-contrib)) (action (chdir %{project_root} @@ -17,7 +16,6 @@ (deps ; This will be replaced soon by `theories/**/*.v` soon, thanks to rgrinberg (source_tree %{project_root}/theories) - (source_tree %{project_root}/plugins) (source_tree %{project_root}/user-contrib) (:header %{project_root}/doc/common/styles/html/coqremote/header.html) (:footer %{project_root}/doc/common/styles/html/coqremote/footer.html) @@ -26,7 +24,7 @@ (action (progn (run mkdir -p html) - (bash "%{bin:coqdoc} -q -d html --with-header %{header} --with-footer %{footer} --multi-index --html -g -R %{project_root}/theories Coq -R %{project_root}/plugins Coq -Q %{project_root}/user-contrib/Ltac2 Ltac2 $(find %{project_root}/theories %{project_root}/plugins %{project_root}/user-contrib -name *.v)") + (bash "%{bin:coqdoc} -q -d html --with-header %{header} --with-footer %{footer} --multi-index --html -g -R %{project_root}/theories Coq -Q %{project_root}/user-contrib/Ltac2 Ltac2 $(find %{project_root}/theories %{project_root}/user-contrib -name *.v)") (run mv html/index.html html/genindex.html) (with-stdout-to _index.html |