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 /lib/aux_file.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 'lib/aux_file.ml')
| -rw-r--r-- | lib/aux_file.ml | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/lib/aux_file.ml b/lib/aux_file.ml index c6c7b4242..0f0f09aa2 100644 --- a/lib/aux_file.ml +++ b/lib/aux_file.ml @@ -17,6 +17,10 @@ let version = 1 let oc = ref None +let chop_extension f = + if check_suffix f ".v" then chop_extension f + else f + let aux_file_name_for vfile = dirname vfile ^ "/." ^ chop_extension(basename vfile) ^ ".aux" |