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

Update GitHub Actions #248

Open
wants to merge 1 commit into
base: main
Choose a base branch
from

Conversation

DimitriPapadopoulos
Copy link
Contributor

No description provided.

@DimitriPapadopoulos
Copy link
Contributor Author

DimitriPapadopoulos commented Dec 24, 2022

Not sure where the "bench_pr / Benchmark (PR)" CI failure comes from. This line:

git reset --hard HEAD

yields:

HEAD is now at 12298c9 Merge d20b5f92ac52215c1e368f03cab86d1d5ec15e59 into b667091a74dc7bbf92c2c061867ab5fdd4cab2b0

Where does 12298c9 come from? A cached erased commit?

@DimitriPapadopoulos
Copy link
Contributor Author

Updating actions/checkout@v1 to actions/checkout@v3 or even actions/checkout@v2 breaks "Benchmark (PR) " CI job. Let's leave it at @v1 for now.

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.

None yet

1 participant