diff options
| author | Rémi Verschelde <rverschelde@gmail.com> | 2018-01-08 20:08:04 +0100 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2018-01-08 20:08:04 +0100 |
| commit | 15cb56122e3275b1b0f5018e03350ec1c2573d4a (patch) | |
| tree | 57d4a45d0bd965b6c79d1483d67ce66fce310541 /thirdparty/misc | |
| parent | 299e490cf4c9cfd72a9e4f53effaa41bf5e0d7df (diff) | |
| parent | 7e1b39245f96d425d5fb64cffef0c29e6c04deaa (diff) | |
Merge pull request #15498 from poke1024/fix15478
Don't delete edit menu too early when closing script tabs
Diffstat (limited to 'thirdparty/misc')
0 files changed, 0 insertions, 0 deletions