diff options
author | Maxime Dénès <mail@maximedenes.fr> | 2017-08-31 14:18:50 +0200 |
---|---|---|
committer | Maxime Dénès <mail@maximedenes.fr> | 2017-08-31 14:18:50 +0200 |
commit | 13fb8de9aff07e4346ca4bdc866507503e9be12e (patch) | |
tree | 3ba390e7b32d0909a92d964a27c94eb9da3214c2 /ide/ide_slave.ml | |
parent | bed414f560e3db511ca3a647acce6e5ebc70b4cc (diff) | |
parent | 86dbe3337197741d0ceaea740cbbd3e8b9b1dfe1 (diff) |
Merge PR #992: Fix BZ#5687: Coqtop died badly modal message box from CoqIDE.
Diffstat (limited to 'ide/ide_slave.ml')
0 files changed, 0 insertions, 0 deletions