diff options
| author | Hugo Herbelin | 2015-07-03 21:25:15 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2015-12-14 22:26:02 +0100 |
| commit | 2ab8455cffef4097a441eb6befaa29f6f3076824 (patch) | |
| tree | b57ae29224dbaf8427bb87d3069c8b521735f579 /plugins/extraction/mlutil.ml | |
| 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 'plugins/extraction/mlutil.ml')
0 files changed, 0 insertions, 0 deletions