Skip to content

Commit 58b2790

Browse files
authored
Merge branch 'main' into docs-port-8.20
2 parents 20bca8c + 0e7e63c commit 58b2790

File tree

16 files changed

+325
-22
lines changed

16 files changed

+325
-22
lines changed

.gitignore

+1-1
Original file line numberDiff line numberDiff line change
@@ -16,4 +16,4 @@ _opam/
1616
.venv/
1717

1818
# Copied documentation
19-
rocq-doc/
19+
rocq-doc

Makefile

+1
Original file line numberDiff line numberDiff line change
@@ -7,6 +7,7 @@ GIT_BRANCH=$(shell git branch --show-current)
77

88
export GIT_COMMIT
99
export GIT_BRANCH
10+
export DOC_PATH
1011

1112
.PHONY: all
1213
all:

asset/logos/darkmode/ipparis.png

6.76 KB
Loading
Loading

asset/logos/lightmode/ipparis.png

3.32 KB
Loading

0 commit comments

Comments
 (0)