aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar Guillaume Melquiond <guillaume.melquiond@inria.fr>2015-06-09 08:06:43 +0200
committerGravatar Guillaume Melquiond <guillaume.melquiond@inria.fr>2015-06-09 08:06:43 +0200
commit0736befd45671875d4c9761fc42f38766a14493b (patch)
treeccee43ba09b342c75fd44f9400fc7792c79c78c7
parent5fab341f70b05823910b9a7ead63deb7b35bf161 (diff)
Support CRLF end of line in fake_ide.
-rw-r--r--tools/fake_ide.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/tools/fake_ide.ml b/tools/fake_ide.ml
index d7a292f4c..a9a7251c5 100644
--- a/tools/fake_ide.ml
+++ b/tools/fake_ide.ml
@@ -90,7 +90,7 @@ module Parser = struct (* {{{ *)
in find ~-1 0
else raise (Err ("Balanced "^String.make 1 c^" not found in: "^s))
- let eat_blanks s = snd (eat_rex "[ \n\t]*") s
+ let eat_blanks s = snd (eat_rex "[ \r\n\t]*") s
let s = ref ""