Skip to content

Commit

Permalink
Fix makefile for doc
Browse files Browse the repository at this point in the history
  • Loading branch information
hferee committed Sep 26, 2024
1 parent 3b0fd30 commit de685c5
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion Makefile
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down

0 comments on commit de685c5

Please sign in to comment.