-
Notifications
You must be signed in to change notification settings - Fork 414
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
Cache causes dune build
to fail when HEAD
doesn't exist
#4429
Comments
Signed-off-by: Craig Ferguson <[email protected]>
Signed-off-by: Craig Ferguson <[email protected]>
Signed-off-by: Craig Ferguson <[email protected]> Signed-off-by: Jeremie Dimino <[email protected]>
Duplicate of #3619 |
Thanks for the report! I found that before but it seemed innocuous - the fact that it can be triggered through the cache makes it a bit more important. |
Ah, apologies for the duplicate; should have looked a bit more closely. As @jeremiedimino and @snowleopard point out in the linked PR, the caching reproduction is likely to go away due to unrelated refactoring, so this isn't such a big problem. It is also possible to observe it via |
This was fixed in #4441 |
The Dune cache uses
Vcs.commit_id
as an input to the Dune cache here. Unfortunately, this commit ID might not always exist: when using Git,HEAD
doesn't exist in commit-less repositories:As of today, this is also triggerable via
dune build
with the cache enabled:As discussed in #4430, the latter case is going away for unrelated reasons.
Obviously only a tiny problem, but seemed worth a bug report.
Reproduction
See #4430.
The text was updated successfully, but these errors were encountered: