diff options
| author | Emilio Jesus Gallego Arias | 2019-03-04 16:47:16 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-03-04 16:47:16 +0100 |
| commit | 11d1c70ce0747d03c849df1362119d4ccaccb443 (patch) | |
| tree | a9337577d0de316ccae439b80a05cb9556900b4c /plugins/syntax | |
| parent | be15d32ad16104c81f4fbf42556067848aa0acec (diff) | |
| parent | 745669e29695b68b0c6aa9dbe27a835e43c87308 (diff) | |
Merge PR #9688: [stm] unfocus when edition exits the proof (fix #9431)
Reviewed-by: ejgallego
Diffstat (limited to 'plugins/syntax')
0 files changed, 0 insertions, 0 deletions