diff --git a/Makefile b/Makefile index 42dce89e16f11b39fe520c646d42a4534dc7cd7b..765eb11c092898e1858aa42379950e48616a3b14 100644 --- a/Makefile +++ b/Makefile @@ -110,6 +110,8 @@ 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'".