Couple of improvements to using a separate bench_repo #431
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
1.Skip installing opam dependencies of the repo when using separate
bench_repo2. Ensure cached
bench_repois used only when thebench_repohas no changes. We use the GitHub refs API to see if the repo has changed, to decide whether to use the cached bench_repo or make a new clone of it. The trick here is from this GitHub issue comment.3. Support specifying a specific branch of the
bench_repoto use for running the benchmarks. The branch can be specified using the/tree/<branch-name>suffix in the bench_repo URL.