search

revng / revng-orchestra

rev.ng's package manager
4 stars 6 forks source link

Run GitHub Actions on pull-requests in this repo #51

Closed depau closed 2 years ago

aleclearmind commented 2 years ago

Please make a single PR for supporting running the CI from pull requests.

depau commented 2 years ago

@aleclearmind this PR has nothing to do with the other one.

EDIT: I see I pushed this commit on the other PR as well, My bad, should I keep it there? EDIT: Now I remember, it was temporary to show you that tests run. So yeah it has nothing to do with the other one.

aleclearmind commented 2 years ago

So we can keep it closed I guess?

depau commented 2 years ago

I think this can be fast-tracked so that the other PRs to orchestra can benefit from it.

The actual changes of #50 can wait until you feel confident to merge them.

depau commented 2 years ago

@aleclearmind As discussed IRL this can be trivially merged and it is independent from the other changes.

aleclearmind commented 2 years ago

Merged in 33c962a.