diff options
| author | Maxime Dénès | 2017-12-05 09:52:09 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2017-12-05 09:52:09 +0100 |
| commit | 04d5253b91f7567a09b950caa420b69fc34c0d0e (patch) | |
| tree | d601128f0ebe23f9ffce44949666ba2f8a3630a9 /dev/include | |
| parent | ecc56d61d2a6b281fe1581e36859158f3ad04fcd (diff) | |
| parent | 2b4ed9b34e3852df7582f2a084274340113194e4 (diff) | |
Merge PR #6302: Uninstall doc dir, not dev (which is not installed), fixes #6007
Diffstat (limited to 'dev/include')
0 files changed, 0 insertions, 0 deletions