Fix the same bug in MLKit for a second time - needs to recognize /r a…

…s a whitespace character. Having /r be a Whitespace and not just a VWhitespace may be a mistake but I don
rowandavies · Sep 29, 2011 · c935267 · c935267
1 parent 5f668e6
commit c935267
Show file tree

Hide file tree

Showing 2 changed files with 1,713 additions and 771 deletions.
diff --git a/src/Parsing/Topdec.lex b/src/Parsing/Topdec.lex
@@ -67,8 +67,8 @@
 	);
 %arg	(arg: UserDeclarations.arg);
 
-WhiteSpace	   = [\ \t]+;
-VWhiteSpace	   = [\ \t\n\012]+;
+WhiteSpace	   = [\ \t\r]+;
+VWhiteSpace	   = [\ \t\r\n\012]+;
 UC		   = [A-Z];
 LC		   = [a-z];
 Letter		   = {UC} | {LC};