Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

ci: Don't build unrelevant documentation tags. #305

Closed
duesee opened this issue Dec 13, 2022 · 0 comments · Fixed by #307
Closed

ci: Don't build unrelevant documentation tags. #305

duesee opened this issue Dec 13, 2022 · 0 comments · Fixed by #307
Assignees
@duesee
Labels
build 🔨 ci 🤖 enhancement New feature or request

Comments

@duesee
Copy link
Contributor

duesee commented Dec 13, 2022

No description provided.

@duesee duesee added enhancement New feature or request build 🔨 ci 🤖 labels Dec 13, 2022
@duesee duesee self-assigned this Dec 13, 2022
@duesee duesee linked a pull request Dec 13, 2022 that will close this issue
docs: Build C documentation for c-... tags and main branch only. #307
Merged
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@duesee duesee

Labels
build 🔨 ci 🤖 enhancement New feature or request
Projects
HACL Packages
Status: Done
Milestone
No milestone
Development

Successfully merging a pull request may close this issue.

docs: Build C documentation for c-... tags and main branch only. cryspen/hacl-packages
1 participant
@duesee