aboutsummaryrefslogtreecommitdiff
path: root/doc/stdlib
diff options
context:
space:
mode:
authorHugo Herbelin2019-07-23 21:25:12 +0200
committerHugo Herbelin2019-07-23 21:47:56 +0200
commit64906d402e9757af850b9562aaae69099abf871f (patch)
tree54158ac1b3e8700c51caaa1a0c34cdf78dfd1f66 /doc/stdlib
parentd57f262bb39ebbcae630f1439377c51aaa41452b (diff)
Fixing #10286 (coqide hangs on invalid filenames).
The hang is caused by a failure in the interpretation by coqtop of the command line option "-topfile filename" (this happens before a proper XML communication is set up between coqtop and coqide). The fix is a bit ad hoc. We copy in coqide the code for checking the validity of a filename. We copy it to avoid adding a dependency in either Names.check_valid or Stm.dirpath_of_file. We do a minimal check (on the basename) while (if it hadn't added extra depencencies or code duplication) it would have been more consistent to do the exact same check as in Stm.dirpath_of_file.
Diffstat (limited to 'doc/stdlib')
0 files changed, 0 insertions, 0 deletions