diff options
| author | Théo Zimmermann | 2020-05-14 15:31:11 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2020-05-14 15:31:11 +0200 |
| commit | 8dd5c47007817c104d57a449409a6b9c6f8ef12e (patch) | |
| tree | 416c8be9d63ea6b21ea66d7a3e1ff47cc132ba4b /dev | |
| parent | 6f2b88649ec0c1e27befe7bcd2cdbec0ccee95d6 (diff) | |
| parent | 122ab27b2b4f02f370826a0a8ade78a0c0b2d416 (diff) | |
Merge PR #12312: Clarify the documentation for merging PRs with overlays
Reviewed-by: Zimmi48
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions