From 2b4645892255107726f95b75a29fb172db606235 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Franc=CC=A7ois=20Pottier?= <francois.pottier@inria.fr>
Date: Fri, 31 Dec 2021 19:25:33 +0100
Subject: [PATCH] Remove the postprocessing of the .css file.

---
 Makefile | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/Makefile b/Makefile
index 765eb11..f72802c 100644
--- a/Makefile
+++ b/Makefile
@@ -102,18 +102,18 @@ publish:
 # Publish an opam description.
 	@ opam publish -v $(DATE) $(THIS_SPACES) $(ARCHIVE)
 
+# ------------------------------------------------------------------------------
+
+# Documentation.
+
 DOCDIR = _build/default/_doc/_html
 DOC    = $(DOCDIR)/index.html
-CSS    = $(DOCDIR)/odoc.css
-
-# ------------------------------------------------------------------------------
 
 .PHONY: doc
 doc:
 	@ rm -rf _build/default/_doc
 	@ dune clean
 	@ dune build @doc
-	@ sed -i.bak 's/font-weight: 500;/font-weight: bold;/' $(CSS) && rm -f $(CSS).bak
 	@ echo "You can view the documentation by typing 'make view'".
 
 .PHONY: view
-- 
GitLab