diff options
| author | Pierre-Marie Pédrot | 2019-08-06 09:56:38 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-08-06 09:56:38 +0200 |
| commit | 823fdc311e700ec2edb6441d5fc6908d58818dd5 (patch) | |
| tree | 45b88f5c17781e28ecdce38b8ef9cbb6c0c01ed9 /plugins | |
| parent | e797e35d137d6cf84591335e60b3668f8f7e64b2 (diff) | |
| parent | 64906d402e9757af850b9562aaae69099abf871f (diff) | |
Merge PR #10557: Fixing #10286 (coqide hangs on invalid filenames)
Ack-by: maximedenes
Reviewed-by: ppedrot
Diffstat (limited to 'plugins')
0 files changed, 0 insertions, 0 deletions