diff options
| author | Théo Zimmermann | 2018-03-23 15:56:23 +0100 |
|---|---|---|
| committer | Théo Zimmermann | 2018-03-23 15:56:23 +0100 |
| commit | 9236c0c40203f132eaa09436b0379d6dde23ddbe (patch) | |
| tree | 902010b0edac3c1c4e20a318fccd718d25197ec1 /dev/include | |
| parent | 4e3819425445c3236f6aca77e95f2ee854cf4417 (diff) | |
| parent | ee62b9269beb78b12f1431816ea1acc0cd09130c (diff) | |
Merge PR #7052: More precise wording about the merge process.
Diffstat (limited to 'dev/include')
0 files changed, 0 insertions, 0 deletions