diff options
| -rwxr-xr-x | tools/coqdep_lexer.mll | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tools/coqdep_lexer.mll b/tools/coqdep_lexer.mll index 2d65c7864..b185e2239 100755 --- a/tools/coqdep_lexer.mll +++ b/tools/coqdep_lexer.mll @@ -37,7 +37,7 @@ let field_name s = String.sub s 1 (String.length s - 1) } -let space = [' ' '\t' '\n'] +let space = [' ' '\t' '\n' '\r'] let lowercase = ['a'-'z' '\223'-'\246' '\248'-'\255'] let uppercase = ['A'-'Z' '\192'-'\214' '\216'-'\222'] let identchar = |