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

Run CI on PRs that come from forks #107

Closed
Julian opened this issue Jul 13, 2023 · 0 comments · Fixed by #127
Closed

Run CI on PRs that come from forks #107

Julian opened this issue Jul 13, 2023 · 0 comments · Fixed by #127

Comments

@Julian
Copy link
Collaborator

Julian commented Jul 13, 2023

Right now, a simple PR like #103 has no CI run on it, so even though it almost certainly builds correctly, there's no feedback for the author that the PDF build is all good.

The workflow right now does both a build and a release, but if it's trivially modified to only do the latter part, then we can run it on all PRs (and throw the PDF away, or just link it from the PR).

I can try to get to this today, but filing in case I forget.
@Julian Julian changed the title Run CI on PRs without doing a release Run CI on PRs that come from forks Jul 13, 2023
Seasawher added a commit to Seasawher/lean4-metaprogramming-book that referenced this issue Jan 13, 2024
@Seasawher
Run CI on PRs that come from forks leanprover-community#107
e112e5f
@Seasawher Seasawher mentioned this issue Jan 13, 2024
Merged
Julian added a commit that referenced this issue Jan 13, 2024
@Julian
Merge pull request #127 from Seasawher/update-ci-trigger
bd6f672 
Run CI on PRs that come from forks #107
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging a pull request may close this issue.

Run CI on PRs that come from forks #107 Seasawher/lean4-metaprogramming-book
1 participant
@Julian