diff --git a/Makefile b/Makefile index 53447dc270..93ec886c78 100644 --- a/Makefile +++ b/Makefile @@ -15,7 +15,7 @@ test : .PHONY : bench bench: - @dune build @bench + @ODOC_BENCHMARK=true dune build @bench .PHONY : coverage coverage : diff --git a/doc/driver.mld b/doc/driver.mld index d18ba0eed3..af792df16b 100644 --- a/doc/driver.mld +++ b/doc/driver.mld @@ -300,14 +300,7 @@ let dep_libraries_core = [ ];; let extra_deps = [ - "base"; - "core_kernel"; - "bin_prot"; - "sexplib"; - "sexplib0"; - "base_quickcheck"; - "ppx_sexp_conv"; - "ppx_hash"; + "core"; ] let dep_libraries = diff --git a/doc/library_mlds/core.mld b/doc/library_mlds/core.mld new file mode 100644 index 0000000000..17c33fa73e --- /dev/null +++ b/doc/library_mlds/core.mld @@ -0,0 +1 @@ +{0 core} diff --git a/odoc-bench.opam b/odoc-bench.opam index be93e104a4..c6b3a08a0f 100644 --- a/odoc-bench.opam +++ b/odoc-bench.opam @@ -41,4 +41,5 @@ depends: [ "bos" "yojson" {>= "1.6.0"} "mdx" {>= "2.3.0"} + "core" ]