diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-07-03 21:25:15 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-12-14 22:26:02 +0100 |
| commit | 2ab8455cffef4097a441eb6befaa29f6f3076824 (patch) | |
| tree | b57ae29224dbaf8427bb87d3069c8b521735f579 /ide | |
| parent | c3aa4c065fac0e37d67ca001aec47b1c2138e648 (diff) | |
Fixing little bug of coq_makefile with unterminated comment.
Force failing when reaching end of file with unterminated comment when
parsing Make (project) file.
Diffstat (limited to 'ide')
| -rw-r--r-- | ide/project_file.ml4 | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/ide/project_file.ml4 b/ide/project_file.ml4 index f7279f9cf..152f76cc0 100644 --- a/ide/project_file.ml4 +++ b/ide/project_file.ml4 @@ -28,6 +28,7 @@ let rec parse_string = parser and parse_string2 = parser | [< ''"' >] -> "" | [< 'c; s >] -> (String.make 1 c)^(parse_string2 s) + | [< >] -> raise Parsing_error and parse_skip_comment = parser | [< ''\n'; s >] -> s | [< 'c; s >] -> parse_skip_comment s |