diff options
| author | Théo Zimmermann | 2019-03-26 16:30:13 +0100 |
|---|---|---|
| committer | Théo Zimmermann | 2019-03-26 16:30:13 +0100 |
| commit | 0ff2e4b9f845ff280ee7adb865f837bc6040efbf (patch) | |
| tree | fcbbd6a4718bf6929a9da217ea64a2ed0e946f1e /dev/base_include | |
| parent | 225d8d3326d12a1f24e8220a3ad0a6a7c5749256 (diff) | |
| parent | 9c821d8dde1d6173a1f2a92f8c98c1c61d81c3c6 (diff) | |
Merge PR #9833: Improve the backport script.
Reviewed-by: Zimmi48
Diffstat (limited to 'dev/base_include')
0 files changed, 0 insertions, 0 deletions