diff options
| author | Pierre-Marie Pédrot | 2018-11-12 13:47:53 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-11-12 13:47:53 +0100 |
| commit | 78ab6a5263d3d0dd4da300fcfb87c5e896acc153 (patch) | |
| tree | 9f0e929522f2c46249200ff4e270833c014c0ec9 /dev/ci | |
| parent | 186d67228018a84a93de024971356249ddbde668 (diff) | |
| parent | a8a3aeb49f3627a65c86c92b0ed743f7bfcf9ffb (diff) | |
Merge PR #8958: [clib] Remove unneeded `get_extension` function.
Diffstat (limited to 'dev/ci')
0 files changed, 0 insertions, 0 deletions