diff options
| author | Emilio Jesus Gallego Arias | 2017-12-09 02:06:41 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2017-12-09 03:18:11 +0100 |
| commit | 751375678bfee0cf3abb05dafe79fcf5689c4fce (patch) | |
| tree | 8b06feec7de3fcd9bc90ed91c5393e3f433daf95 /kernel/typeops.ml | |
| parent | 7b40908bfbc255d51384e88a73fa5d98380b237f (diff) | |
[ci] Download ci-sf archives into the proper CI build dir.
Currently, `make ci-sf` downloads and builds the files in the main root
directory. we fix that.
Diffstat (limited to 'kernel/typeops.ml')
0 files changed, 0 insertions, 0 deletions