aboutsummaryrefslogtreecommitdiff
path: root/ide
diff options
context:
space:
mode:
Diffstat (limited to 'ide')
-rw-r--r--ide/coqide.ml8
1 files changed, 7 insertions, 1 deletions
diff --git a/ide/coqide.ml b/ide/coqide.ml
index 00168a06b1..9cdfd0dc21 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -110,7 +110,13 @@ let make_coqtop_args fname =
| None -> args
| Some fname ->
if List.exists (String.equal "-top") args then args
- else "-topfile"::fname::args
+ else
+ (* We basically copy the code of Names.check_valid since it is not exported *)
+ (* to coqide. This is to prevent a possible failure of parsing "-topfile" *)
+ (* at initialization of coqtop (see #10286) *)
+ match Unicode.ident_refutation (Filename.chop_extension (Filename.basename fname)) with
+ | Some (_,x) -> output_string stderr (x^"\n"); exit 1
+ | None -> "-topfile"::fname::args
in
proj, args