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 /kernel/univ.ml | |
| 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 'kernel/univ.ml')
0 files changed, 0 insertions, 0 deletions