Skip to content

GitHub Actions: build documentation of AdditiveClosuresForCAP - #1759

Closed
TKuh wants to merge 1 commit into
homalg-project:masterfrom
TKuh:ci_add_closure_pkg
Closed

GitHub Actions: build documentation of AdditiveClosuresForCAP#1759
TKuh wants to merge 1 commit into
homalg-project:masterfrom
TKuh:ci_add_closure_pkg

Conversation

@TKuh

@TKuh TKuh commented Jul 1, 2025

Copy link
Copy Markdown
Collaborator

No description provided.

@mohamed-barakat

Copy link
Copy Markdown
Member

Shouldn't this be part of the original PR?

@TKuh

TKuh commented Jul 1, 2025

Copy link
Copy Markdown
Collaborator Author

But does the CI then immediately use the new workflow? I thought it would execute the new PR with its old workflow.

It shouldn't do any harm, since

if [ -d "CAP_project/AdditiveClosuresForCAP" ];

executes only if the directory AdditiveClosuresForCAP exists anyway.

@TKuh

TKuh commented Jul 1, 2025

Copy link
Copy Markdown
Collaborator Author

Uploading to Codecov fails.

@kamalsaleh

Copy link
Copy Markdown
Member

Uploading to Codecov fails—or takes too long—because the CODECOV_TOKEN secret is, for security reasons, not available in pull requests from external forks. It’s only accessible during push events or pull requests originating from a branch within the same repository. This is why GitHub Actions often run faster once a PR has been merged.

About the workflow file: I believe GitHub-Actions will use the updated version of the workflow file. So what Mohamed suggested about including the line in your original PR is actually valid.

@TKuh

TKuh commented Jul 1, 2025

Copy link
Copy Markdown
Collaborator Author

Uploading to Codecov fails—or takes too long—because the CODECOV_TOKEN secret is, for security reasons, not available in pull requests from external forks. It’s only accessible during push events or pull requests originating from a branch within the same repository. This is why GitHub Actions often run faster once a PR has been merged.

So it will always fail for my PR's? :)

About the workflow file: I believe GitHub-Actions will use the updated version of the workflow file. So what Mohamed suggested about including the line in your original PR is actually valid.

Ok, thank you. But I leave this PR open for now, just in case.

@kamalsaleh

kamalsaleh commented Jul 1, 2025

Copy link
Copy Markdown
Member

Uploading to Codecov fails—or takes too long—because the CODECOV_TOKEN secret is, for security reasons, not available in pull requests from external forks. It’s only accessible during push events or pull requests originating from a branch within the same repository. This is why GitHub Actions often run faster once a PR has been merged.

So it will always fail for my PR's? :)

Yes, it fails until eventually after 1 hour it succeeds :-)

@TKuh TKuh closed this Jul 1, 2025
@TKuh
TKuh deleted the ci_add_closure_pkg branch July 1, 2025 19:37
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants