diff options
author | Maxime Dénès <mail@maximedenes.fr> | 2016-11-29 16:35:56 +0100 |
---|---|---|
committer | Maxime Dénès <mail@maximedenes.fr> | 2016-11-30 09:39:45 +0100 |
commit | 3e6fa1cbdc0ec145728089000595b6ea29f37a4c (patch) | |
tree | 1441c8d1ceb8f4116ce06e74635cbf0da26a8459 /test-suite/success/cc.v | |
parent | b6a70501e7ba46d556288abc5c3c81399a280e26 (diff) |
Fix #5183 - Two CoqIDE crash errors
When opening a file without extension, an uncaught exception was
occurring.
Note that this fix is not complete, since the "Compile Buffer" command
still fails. This is because of a limitation of coqc which appends the
".v" extension to its argument even if it already existed (and even if
it doesn't exist with the extension!).
Diffstat (limited to 'test-suite/success/cc.v')
0 files changed, 0 insertions, 0 deletions