diff options
| author | Rémi Verschelde <rverschelde@gmail.com> | 2020-02-26 10:09:43 +0100 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-02-26 10:09:43 +0100 |
| commit | 3a4c128f07cb744ed37529d8206e04cd0fa2e374 (patch) | |
| tree | a85530c55c2fbaa9502a1136298e0cba4b8c594c /thirdparty | |
| parent | fc5a400ce28c600da6ff4c40941e81d8ee588e53 (diff) | |
| parent | c143b5c6770c690e46545e17c7b28bee698e5a3a (diff) | |
Merge pull request #36551 from AndreaCatania/navigation_destruction_flush
Flushes commands just before the navigation server is destroyed
Diffstat (limited to 'thirdparty')
0 files changed, 0 insertions, 0 deletions