diff options
| author | Théo Zimmermann | 2019-02-18 15:32:42 +0100 |
|---|---|---|
| committer | Théo Zimmermann | 2019-02-18 15:33:10 +0100 |
| commit | 7e03019c888161cb027dd76c3fa393d3d8f442e5 (patch) | |
| tree | 59a4f2ef64c72f56ba53b6101ea1f78310ef9785 /pretyping/typeclasses_errors.ml | |
| parent | 77b454e5ab8698f0d87bdf2eb32b48ab998ba590 (diff) | |
[ci] Resolve commit corresponding to branch when downloading tarball.
This ensures that the log will contain the commit hash that we tested.
This reuses the method from the Windows build script (we have a number
of common functions, it would be interesting to start a bash shared
library file).
Diffstat (limited to 'pretyping/typeclasses_errors.ml')
0 files changed, 0 insertions, 0 deletions