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/document.mli | |
| parent | bed414f560e3db511ca3a647acce6e5ebc70b4cc (diff) | |
| parent | 86dbe3337197741d0ceaea740cbbd3e8b9b1dfe1 (diff) | |
Merge PR #992: Fix BZ#5687: Coqtop died badly modal message box from CoqIDE.
Diffstat (limited to 'ide/document.mli')
0 files changed, 0 insertions, 0 deletions