search

project-everest / everest-ci

CI scripts for project everest
3 stars 8 forks source link

offer an option to regenerate the hints for non-master branches #13

Closed msprotz closed 7 years ago

msprotz commented 7 years ago

the script enforces that the branch is master but we may want to be more generic than that

darrenge commented 7 years ago

Is this valid any more? Looking at refresh_hints() in ci, it has "$CI_BRANCH" through out

msprotz commented 7 years ago

Yes, I eventually added that... this has to be triggered through VSTS's UI but theoretically it should work. I think it's just untested. Do you want to try it out on c_relational-ci_r3?

msprotz commented 7 years ago

For F*, that is

darrenge commented 7 years ago

Fired off FStar-Nightly-Linux build ...

msprotz commented 7 years ago

That worked. Thanks for the test! Closing.