From f7a695d36252e4e8adad0a4c3743e4141a4697a5 Mon Sep 17 00:00:00 2001
From: Jules Aguillon <jules@j3s.fr>
Date: Thu, 26 Oct 2023 15:05:58 +0200
Subject: [PATCH] driver.mld: Benchmark building 'core'

Currently, the benchmarks are running the driver with no extra work.
---
 Makefile                  | 2 +-
 doc/driver.mld            | 9 +--------
 doc/library_mlds/core.mld | 1 +
 odoc-bench.opam           | 1 +
 4 files changed, 4 insertions(+), 9 deletions(-)
 create mode 100644 doc/library_mlds/core.mld

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"
 ]