diff options
| author | Enrico Tassi | 2014-01-06 17:59:06 +0100 |
|---|---|---|
| committer | Enrico Tassi | 2014-01-06 17:59:06 +0100 |
| commit | 27d9da372a1c407221e687d9fb0d08fc6fca805f (patch) | |
| tree | 16c80c474d048217c25d5ea175728612ee2b9ee1 /dev | |
| parent | 352ce04861c5dd849d20832a8fa0379ea8f43c8c (diff) | |
CoqIDE: do not unfocus if not needed on errors (closes: 3197)
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions