Closed punchagan closed 1 year ago
I think we can ship with the FIXME regarding github assumption for the time being, and add an issue to
git clone
properly from other sources afterward
Yes, I agree. That was my intention too, with adding the FIXME.
Thanks for the review and the merge, @ElectreAAS!
1.Skip installing opam dependencies of the repo when using separate
bench_repo
bench_repo
is used only when thebench_repo
has 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.bench_repo
to use for running the benchmarks. The branch can be specified using the/tree/<branch-name>
suffix in the bench_repo URL.