diff options
| author | Gaëtan Gilbert | 2017-12-30 20:06:26 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2018-01-08 11:52:38 +0100 |
| commit | 17067aac03eabb8369d587dc91b622642b2673f8 (patch) | |
| tree | c6e3ab448914d44221fe4fdf64dc0ab33773341c /kernel/declarations.ml | |
| parent | 2b28380d1d04c0dc2d0899ba3f3489e29015a6fa (diff) | |
github-check-prs.py: command line option to get token from a file
Diffstat (limited to 'kernel/declarations.ml')
0 files changed, 0 insertions, 0 deletions