From de685c541c5434d42290e3b202db13b87d98eea6 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Hugo=20F=C3=A9r=C3=A9e?= Date: Thu, 26 Sep 2024 14:57:38 +0200 Subject: [PATCH] Fix makefile for doc --- Makefile | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Makefile b/Makefile index 5fe3de8..6d41077 100644 --- a/Makefile +++ b/Makefile @@ -18,8 +18,8 @@ makefile.coq: doc: makefile.coq demo + rm -fr html docs mkdir docs - rm -fr html docs/* COQDOCEXTRAFLAGS='--external $(PUBLIC_URL)' @$(MAKE) -f makefile.coq html cp html/* _build/default/bin/uiml_demo.bc.js docs