From 2ab8455cffef4097a441eb6befaa29f6f3076824 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Fri, 3 Jul 2015 21:25:15 +0200
Subject: Fixing little bug of coq_makefile with unterminated comment.

Force failing when reaching end of file with unterminated comment when
parsing Make (project) file.
---
 ide/project_file.ml4 | 1 +
 1 file changed, 1 insertion(+)

diff --git a/ide/project_file.ml4 b/ide/project_file.ml4
index f7279f9cfe..152f76cc0e 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
-- 
cgit v1.2.3