diff options
| author | coqbot-app[bot] | 2020-10-01 17:55:45 +0000 |
|---|---|---|
| committer | GitHub | 2020-10-01 17:55:45 +0000 |
| commit | b842e83ce941c995dfb266eee33c73e565785554 (patch) | |
| tree | d7e90d993517f1ed5b4659880ecb0e12fa9a6c79 /dev/tools/github-check-prs.py | |
| parent | 7ffb5e663784fffb2cd6aae87bc38a5dc2f37710 (diff) | |
| parent | 0fa5751429e92f6555e9cbe3e3509fec658b879c (diff) | |
Merge PR #13116: interp_context_evars: removed unused [shift] argument
Reviewed-by: ejgallego
Diffstat (limited to 'dev/tools/github-check-prs.py')
0 files changed, 0 insertions, 0 deletions