diff options
| author | Pierre-Marie Pédrot | 2019-09-13 22:15:00 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-09-13 22:15:00 +0200 |
| commit | 3d7de72f45ae2f8bcedbe1db0eb8870e58757b45 (patch) | |
| tree | d07dd344d57290847c14980023b0febd48321922 /plugins | |
| parent | 592f2155f97441022f6b9e238563c8d7794ce60f (diff) | |
| parent | b7a9d3e02b01124179f5a9cdf217a4f4f13d8c24 (diff) | |
Merge PR #10748: Hack for fixing #10578: handle between the three main CoqIDE windows not always set at the expected position
Reviewed-by: ppedrot
Reviewed-by: silene
Diffstat (limited to 'plugins')
0 files changed, 0 insertions, 0 deletions