aboutsummaryrefslogtreecommitdiffhomepage
path: root/ide/config_lexer.mll
diff options
context:
space:
mode:
authorGravatar glondu <glondu@85f007b7-540e-0410-9357-904b9bb8a0f7>2009-09-17 15:58:14 +0000
committerGravatar glondu <glondu@85f007b7-540e-0410-9357-904b9bb8a0f7>2009-09-17 15:58:14 +0000
commit61ccbc81a2f3b4662ed4a2bad9d07d2003dda3a2 (patch)
tree961cc88c714aa91a0276ea9fbf8bc53b2b9d5c28 /ide/config_lexer.mll
parent6d3fbdf36c6a47b49c2a4b16f498972c93c07574 (diff)
Delete trailing whitespaces in all *.{v,ml*} files
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12337 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'ide/config_lexer.mll')
-rw-r--r--ide/config_lexer.mll8
1 files changed, 4 insertions, 4 deletions
diff --git a/ide/config_lexer.mll b/ide/config_lexer.mll
index 8e04331c1..97aeb2f5a 100644
--- a/ide/config_lexer.mll
+++ b/ide/config_lexer.mll
@@ -28,19 +28,19 @@ rule token = parse
| '#' [^ '\n']* { token lexbuf }
| ident { IDENT (lexeme lexbuf) }
| '=' { EQUAL }
- | '"' { Buffer.reset string_buffer;
+ | '"' { Buffer.reset string_buffer;
Buffer.add_char string_buffer '"';
string lexbuf;
let s = Buffer.contents string_buffer in
STRING (Scanf.sscanf s "%S" (fun s -> s)) }
| _ { let c = lexeme_start lexbuf in
- eprintf ".coqiderc: invalid character (%d)\n@." c;
+ eprintf ".coqiderc: invalid character (%d)\n@." c;
token lexbuf }
| eof { EOF }
and string = parse
| '"' { Buffer.add_char string_buffer '"' }
- | '\\' '"' | _
+ | '\\' '"' | _
{ Buffer.add_string string_buffer (lexeme lexbuf); string lexbuf }
| eof { eprintf ".coqiderc: unterminated string\n@." }
@@ -60,7 +60,7 @@ and string = parse
| [] -> ()
| s :: sl -> fprintf fmt "%S@ %a" s print_list sl
in
- Stringmap.iter
+ Stringmap.iter
(fun k s -> fprintf fmt "@[<hov 2>%s = %a@]@\n" k print_list s) m;
fprintf fmt "@.";
close_out c