diff options
| author | Gaëtan Gilbert | 2017-09-20 15:11:08 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2017-09-20 15:11:08 +0200 |
| commit | cb121381aea4eff595ee9322fa8dca9959e51a59 (patch) | |
| tree | 59a9ff4fefc5927cec64f99d079af8ad96693f07 /kernel/cbytecodes.ml | |
| parent | 9933871efd122163f7e2dfe8377b9b2dd384b47b (diff) | |
In gitlab set TRAVIS_BRANCH so user overlays will work as expected.
Diffstat (limited to 'kernel/cbytecodes.ml')
0 files changed, 0 insertions, 0 deletions