diff --git a/Makefile b/Makefile index 765eb11c092898e1858aa42379950e48616a3b14..f72802c4bcfd1c433af9c077aba7acc6ce568d5c 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