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.

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

Move pinefarm out #167

Merged
merged 1 commit into from
Dec 20, 2022
Merged

Move pinefarm out #167

merged 1 commit into from
Dec 20, 2022

Conversation

alecandido
Copy link
Member

I just moved everything to https://github.com/NNPDF/pinefarm

I kept here just the pinecards top-level, and a minimal README.md (feel free to improve it).

@alecandido
Copy link
Member Author

I can transfer issues, and I will do, but I can not transfer PRs. However, the only two PRs that are related to pinefarm (as opposed to just providing/fixing pinecards themselves) are #166 #159, they will have to be moved manually.

@alecandido alecandido linked an issue Dec 14, 2022 that may be closed by this pull request
@scarlehoff
Copy link
Member

Can PR be transferred using the github site? I guess they need to be repushed, rebased or whatever the term is.

@alecandido
Copy link
Member Author

Can PR be transferred using the github site? I guess they need to be repushed, rebased or whatever the term is.

I believe you can't, because it is a completely different Git repo, not even a fork.
You can open a new PR, from this repo targeting that one, but I'm not sure if you can do it if it's not a fork.

At the bare Git level, it is cumbersome as well, but you can take an instance of this repo, add pinefarm as a remote, push the branch there, and open the PR. I'm what is the easiest option.

@felixhekhorn
Copy link
Contributor

felixhekhorn commented Dec 15, 2022

I can transfer issues, and I will do, but I can not transfer PRs. However, the only two PRs that are related to pinefarm (as opposed to just providing/fixing pinecards themselves) are #166 #159, they will have to be moved manually.

also #161 has to be moved

EDIT: more precisely: the script part (that will result into a package sooner or later)

@scarlehoff
Copy link
Member

Shouldn't we merge this?

@alecandido
Copy link
Member Author

alecandido commented Dec 20, 2022

Shouldn't we merge this?

I was waiting for full approval, i.e. at least you @scarlehoff and @cschwan as well. (If you wish also you @andreab1997, but you worked little in here, so you don't have to)

@alecandido alecandido merged commit 11be4f9 into master Dec 20, 2022
@felixhekhorn felixhekhorn deleted the export-pinefarm branch January 5, 2023 11:12
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.

Split runcards and runner?
4 participants